Follow
Andrew Reynolds
Title
Cited by
Cited by
Year
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
T Liang, A Reynolds, C Tinelli, C Barrett, M Deters
Computer Aided Verification: 26th International Conference, CAV 2014, Held …, 2014
1532014
Counterexample-guided quantifier instantiation for synthesis in SMT
A Reynolds, M Deters, V Kuncak, C Tinelli, C Barrett
Computer Aided Verification: 27th International Conference, CAV 2015, San …, 2015
1522015
Induction for SMT solvers
A Reynolds, V Kuncak
Verification, Model Checking, and Abstract Interpretation: 16th …, 2015
1072015
Quantifier instantiation techniques for finite model finding in SMT
A Reynolds, C Tinelli, A Goel, S Krstić, M Deters, C Barrett
Automated Deduction–CADE-24: 24th International Conference on Automated …, 2013
822013
SMTCoq: A plug-in for integrating SMT solvers into Coq
B Ekici, A Mebsout, C Tinelli, C Keller, G Katz, A Reynolds, C Barrett
Computer Aided Verification: 29th International Conference, CAV 2017 …, 2017
812017
Finding conflicting instances of quantified formulas in SMT
A Reynolds, C Tinelli, L De Moura
2014 Formal Methods in Computer-Aided Design (FMCAD), 195-202, 2014
792014
SMT proof checking using a logical framework
A Stump, D Oe, A Reynolds, L Hadarean, C Tinelli
Formal Methods in System Design 42, 91-118, 2013
762013
Finite model finding in SMT
A Reynolds, C Tinelli, A Goel, S Krstić
Computer Aided Verification: 25th International Conference, CAV 2013, Saint …, 2013
722013
cvc5: A versatile and industrial-strength SMT solver
H Barbosa, C Barrett, M Brain, G Kremer, H Lachnitt, M Mann, ...
Tools and Algorithms for the Construction and Analysis of Systems: 28th …, 2022
692022
An efficient SMT solver for string constraints
T Liang, A Reynolds, N Tsiskaridze, C Tinelli, C Barrett, M Deters
Formal Methods in System Design 48, 206-234, 2016
602016
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
A Reynolds, H Barbosa, A Nötzli, C Barrett, C Tinelli
Computer Aided Verification: 31st International Conference, CAV 2019, New …, 2019
552019
A tour of CVC4: how it works, and how to use it
M Deters, A Reynolds, T King, C Barrett, C Tinelli
2014 Formal Methods in Computer-Aided Design (FMCAD), 7-7, 2014
542014
Revisiting enumerative instantiation
A Reynolds, H Barbosa, P Fontaine
Tools and Algorithms for the Construction and Analysis of Systems: 24th …, 2018
532018
A decision procedure for (co) datatypes in SMT solvers
A Reynolds, JC Blanchette
Automated Deduction-CADE-25: 25th International Conference on Automated …, 2015
482015
Extending SMT solvers to higher-order logic
H Barbosa, A Reynolds, D El Ouraoui, C Tinelli, C Barrett
Automated Deduction–CADE 27: 27th International Conference on Automated …, 2019
47*2019
Congruence closure with free variables
H Barbosa, P Fontaine, A Reynolds
Tools and Algorithms for the Construction and Analysis of Systems: 23rd …, 2017
432017
A decision procedure for separation logic in SMT
A Reynolds, R Iosif, C Serban, T King
Automated Technology for Verification and Analysis: 14th International …, 2016
412016
Solving quantified linear arithmetic by counterexample-guided instantiation
A Reynolds, T King, V Kuncak
Formal Methods in System Design 51, 500-532, 2017
39*2017
Scaling up DPLL (T) string solvers using context-dependent simplification
A Reynolds, M Woo, C Barrett, D Brumley, T Liang, C Tinelli
Computer Aided Verification: 29th International Conference, CAV 2017 …, 2017
382017
Solving quantified bit-vectors using invertibility conditions
A Niemetz, M Preiner, A Reynolds, C Barrett, C Tinelli
Computer Aided Verification: 30th International Conference, CAV 2018, Held …, 2018
362018
The system can't perform the operation now. Try again later.
Articles 1–20