BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Germany
1 × India
1 × Russia
3 × USA
Collaborated with:
C.Tinelli C.W.Barrett J.C.Blanchette V.Kuncak M.Deters H.Barbosa A.Niemetz M.Preiner C.Barrett K.Bansal A.Nötzli A.Goel S.Krstic T.Liang T.King S.Cruanes B.Meng T.Wies A.Viswanathan D.E.Ouraoui M.Woo D.Brumley Y.Zohar M.Brain B.Ekici A.Mebsout C.Keller G.Katz C.L.Conway L.Hadarean D.Jovanovic
Talks about:
smt (13) solver (7) constraint (3) quantifi (3) theori (3) string (3) model (3) finit (3) find (3) synthesi (2)

Person: Andrew Reynolds

DBLP DBLP: Reynolds:Andrew

Contributed to:

CADE 20152015
CAV 20152015
VMCAI 20152015
CAV 20142014
CADE 20132013
CAV 20132013
CAV 20112011
IJCAR 20162016
CADE 20172017
CAV (2) 20172017
CAV (2) 20182018
IJCAR 20182018
CADE 20192019
CAV (2) 20192019

Wrote 20 papers:

CADE-2015-ReynoldsB #data type #smt
A Decision Procedure for (Co)datatypes in SMT Solvers (AR, JCB), pp. 197–213.
Deciding Local Theory Extensions via E-matching (KB, AR, TK, CWB, TW), pp. 87–105.
CAV-2015-ReynoldsDKTB #quantifier #smt #synthesis
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT (AR, MD, VK, CT, CWB), pp. 198–216.
VMCAI-2015-ReynoldsK #induction #smt
Induction for SMT Solvers (AR, VK), pp. 80–98.
CAV-2014-LiangRTBD #formal method #regular expression #string
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (TL, AR, CT, CB, MD), pp. 646–662.
CADE-2013-ReynoldsTGKDB #finite #quantifier #smt
Quantifier Instantiation Techniques for Finite Model Finding in SMT (AR, CT, AG, SK, MD, CB), pp. 377–391.
CAV-2013-ReynoldsTGK #finite #smt
Finite Model Finding in SMT (AR, CT, AG, SK), pp. 640–655.
CVC4 (CB, CLC, MD, LH, DJ, TK, AR, CT), pp. 171–177.
IJCAR-2016-BansalRBT #constraints #finite #set #smt
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (KB, AR, CWB, CT), pp. 82–98.
IJCAR-2016-ReynoldsBCT #recursion #smt
Model Finding for Recursive Functions in SMT (AR, JCB, SC, CT), pp. 133–151.
CADE-2017-MengRTB #constraints #relational #smt #theorem proving
Relational Constraint Solving in SMT (BM, AR, CT, CWB), pp. 148–165.
CAV-2017-EkiciMTKKRB #coq #named #plugin #smt
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (BE, AM, CT, CK, GK, AR, CWB), pp. 126–133.
CAV-2017-ReynoldsWBBLT #scalability #string #using
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification (AR, MW, CWB, DB, TL, CT), pp. 453–474.
CAV-2018-NiemetzPRBT #quantifier #using
Solving Quantified Bit-Vectors Using Invertibility Conditions (AN, MP, AR, CWB, CT), pp. 236–255.
IJCAR-2018-ReynoldsVBTB #data type
Datatypes with Shared Selectors (AR, AV, HB, CT, CWB), pp. 591–608.
CADE-2019-BarbosaROTB #higher-order #logic #smt
Extending SMT Solvers to Higher-Order Logic (HB, AR, DEO, CT, CWB), pp. 35–54.
CADE-2019-NiemetzPRZBT #independence #proving #smt #towards
Towards Bit-Width-Independent Proofs in SMT Solvers (AN, MP, AR, YZ, CWB, CT), pp. 366–384.
CAV-2019-BrainNPRBT #float
Invertibility Conditions for Floating-Point Formulas (MB, AN, MP, AR, CWB, CT), pp. 116–136.
CAV-2019-ReynoldsBNBT #named #performance #synthesis
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (AR, HB, AN, CWB, CT), pp. 74–83.
CAV-2019-ReynoldsNBT #abstraction #constraints #smt #string
High-Level Abstractions for Simplifying Extended String Constraints in SMT (AR, AN, CWB, CT), pp. 23–42.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.