BibSLEIGH — Andrew

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: Reynolds:Andrew

Contributed to:

2015

2014

2013

2011

2016

2017

2018

2019

Wrote 20 papers:

CADE-2015-ReynoldsB #data type #smt: A Decision Procedure for (Co)datatypes in SMT Solvers (AR, JCB), pp. 197–213.
CAV-2015-BansalR0BW: 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.
CAV-2011-BarrettCDHJKRT: 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.