Andrew Reynolds
Titre
Citée par
Citée par
Année
Cvc4
C Barrett, CL Conway, M Deters, L Hadarean, D Jovanović, T King, ...
International Conference on Computer Aided Verification, 171-177, 2011
11322011
A DPLL (T) theory solver for a theory of strings and regular expressions
T Liang, A Reynolds, C Tinelli, C Barrett, M Deters
International Conference on Computer Aided Verification, 646-662, 2014
1322014
Counterexample-guided quantifier instantiation for synthesis in SMT
A Reynolds, M Deters, V Kuncak, C Tinelli, C Barrett
International Conference on Computer Aided Verification, 198-216, 2015
1302015
Induction for SMT solvers
A Reynolds, V Kuncak
International Workshop on Verification, Model Checking, and Abstract …, 2015
812015
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
752014
Quantifier instantiation techniques for finite model finding in SMT
A Reynolds, C Tinelli, A Goel, S Krstić, M Deters, C Barrett
International Conference on Automated Deduction, 377-391, 2013
722013
Finite model finding in SMT
A Reynolds, C Tinelli, A Goel, S Krstić
International Conference on Computer Aided Verification, 640-655, 2013
652013
SMTCoq: A plug-in for integrating SMT solvers into Coq
B Ekici, A Mebsout, C Tinelli, C Keller, G Katz, A Reynolds, C Barrett
International Conference on Computer Aided Verification, 126-133, 2017
602017
SMT proof checking using a logical framework
A Stump, D Oe, A Reynolds, L Hadarean, C Tinelli
Formal Methods in System Design 42 (1), 91-118, 2013
602013
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
492014
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 (3), 206-234, 2016
472016
A decision procedure for (co) datatypes in SMT solvers
A Reynolds, JC Blanchette
International Conference on Automated Deduction, 197-213, 2015
402015
Revisiting enumerative instantiation
A Reynolds, H Barbosa, P Fontaine
International Conference on Tools and Algorithms for the Construction and …, 2018
382018
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
A Reynolds, H Barbosa, A Nötzli, C Barrett, C Tinelli
International Conference on Computer Aided Verification, 74-83, 2019
352019
Congruence closure with free variables
H Barbosa, P Fontaine, A Reynolds
International Conference on Tools and Algorithms for the Construction and …, 2017
342017
A decision procedure for separation logic in SMT
A Reynolds, R Iosif, C Serban, T King
International Symposium on Automated Technology for Verification and …, 2016
342016
Extending SMT solvers to higher-order logic
H Barbosa, A Reynolds, D El Ouraoui, C Tinelli, C Barrett
International Conference on Automated Deduction, 35-54, 2019
33*2019
Solving quantified linear arithmetic by counterexample-guided instantiation
A Reynolds, T King, V Kuncak
Formal Methods in System Design 51 (3), 500-532, 2017
33*2017
Solving quantified bit-vectors using invertibility conditions
A Niemetz, M Preiner, A Reynolds, C Barrett, C Tinelli
International Conference on Computer Aided Verification, 236-255, 2018
262018
Scaling up DPLL (T) string solvers using context-dependent simplification
A Reynolds, M Woo, C Barrett, D Brumley, T Liang, C Tinelli
International Conference on Computer Aided Verification, 453-474, 2017
262017
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20