default search action
Andrew Reynolds 0001
Andrew J. Reynolds
Person information
- affiliation: University of Iowa, Department of Computer Science, Iowa City, USA
Other persons with the same name
- Andrew Reynolds 0002 — New America Foundation, Washington, DC, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [c67]Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni:
The SemGuS Toolkit. CAV (3) 2024: 27-40 - [c66]Clark W. Barrett
, Cesare Tinelli
Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) 2024: 571-596 - [c65]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL queries using theories of tables and relations. LPAR 2024: 445-463 - [c64]Hanna Lachnitt
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) 2024: 311-330 - [e1]Andrew Reynolds, Serdar Tasiran:
Verified Software. Theories, Tools and Experiments - 15th International Conference, VSTTE 2023, Ames, IA, USA, October 23-24, 2023, Revised Selected Papers. Lecture Notes in Computer Science 14095, Springer 2024, ISBN 978-3-031-66063-4 [contents] - [i21]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL Queries using Theories of Tables and Relations. CoRR abs/2405.03057 (2024) - [i20]Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni:
The SemGuS Toolkit. CoRR abs/2406.01792 (2024) - 2023
- [j13]Haniel Barbosa, Clark W. Barrett
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66(10): 86-95 (2023) - [j12]Alessandro Abate, Haniel Barbosa, Clark W. Barrett
Synthesising Programs with Non-trivial Constants. J. Autom. Reason. 67(2): 19 (2023) - [j11]Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67(3): 32 (2023) - [j10]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett
Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. 67(4): 34 (2023) - [c63]Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. FMCAD 2023: 189-198 - [c62]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. FMCAD 2023: 199-208 - [c61]Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett:
An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR 2023: 11-22 - [c60]Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds:
Selecting Quantifiers for Instantiation in SMT. SMT 2023: 71-77 - [c59]Hanna Lachnitt, Mathias Fleury
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT 2023: 78 - [i19]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. CoRR abs/2306.05854 (2023) - [i18]Saswat Padhi, Elizabeth Polgreen, Mukund Raghothaman, Andrew Reynolds, Abhishek Udupa:
The SyGuS Language Standard Version 2.1. CoRR abs/2312.06001 (2023) - 2022
- [c58]Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR 2022: 15-35 - [c57]Gereon Kremer
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). IJCAR 2022: 95-105 - [c56]Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR 2022: 125-143 - [c55]Andres Nötzli
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) 2022: 205-226 - [c54]Andres Nötzli, Haniel Barbosa, Aina Niemetz
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD 2022: 65-74 - [c53]Haniel Barbosa
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) 2022: 415-442 - [c52]Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia:
Satisfiability and Synthesis Modulo Oracles. VMCAI 2022: 263-284 - [c51]Yoni Zohar
Bit-Precise Reasoning via Int-Blasting. VMCAI 2022: 496-518 - [i17]Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors using an SMT Theory of Sequences. CoRR abs/2205.08095 (2022) - 2021
- [j9]Aina Niemetz
On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. 57(1): 87-115 (2021) - [j8]Aina Niemetz
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65(7): 1001-1025 (2021) - [c50]Ying Sheng
Politeness and Stable Infiniteness: Stronger Together. CADE 2021: 148-165 - [c49]Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD 2021: 256-260 - [c48]Jan Jakubuv, Mikolás Janota, Andrew Reynolds:
Characteristic Subsets of SMT-LIB Benchmarks. SMT 2021: 53-63 - [c47]Aina Niemetz
Syntax-Guided Quantifier Instantiation. TACAS (2) 2021: 145-163 - [d1]Aina Niemetz
Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact). Zenodo, 2021 - [i16]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CoRR abs/2104.11738 (2021) - [i15]Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett:
lazybvtoint at the SMT Competition 2020. CoRR abs/2105.09743 (2021) - [i14]Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR abs/2105.13700 (2021) - [i13]Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia:
Satisfiability and Synthesis Modulo Oracles. CoRR abs/2107.13477 (2021) - 2020
- [c46]Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) 2020: 141-160 - [c45]Andrew Reynolds
A Decision Procedure for String to Code Point Conversion. IJCAR (1) 2020: 218-237 - [c44]M. Fareed Arif, Daniel Larraz
SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. FMCAD 2020: 93-103 - [c43]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
Reductions for Strings and Regular Expressions Revisited. FMCAD 2020: 225-235
2010 – 2019
- 2019
- [j7]Andrew Reynolds, Viktor Kuncak, Cesare Tinelli
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55(2): 73-102 (2019) - [c42]Haniel Barbosa
Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54 - [c41]Aina Niemetz
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE 2019: 366-384 - [c40]Andrew Reynolds
High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) 2019: 23-42 - [c39]Andrew Reynolds, Haniel Barbosa
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) 2019: 74-83 - [c38]Martin Brain
Invertibility Conditions for Floating-Point Formulas. CAV (2) 2019: 116-136 - [c37]Haniel Barbosa, Andrew Reynolds, Daniel Larraz
Extending enumerative function synthesis via SMT-driven classification. FMCAD 2019: 212-220 - [c36]Andres Nötzli
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT 2019: 279-297 - [c35]Mihaela Sighireanu, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan
SL-COMP: Competition of Solvers for Separation Logic. TACAS (3) 2019: 116-132 - [i12]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR abs/1905.10434 (2019) - [i11]Andrew Reynolds, Haniel Barbosa
CVC4SY for SyGuS-COMP 2019. CoRR abs/1907.10175 (2019) - 2018
- [j6]Kshitij Bansal, Clark W. Barrett
Reasoning with Finite Sets and Cardinality Constraints in SMT. Log. Methods Comput. Sci. 14(4) (2018) - [c34]Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa
Datatypes with Shared Selectors. IJCAR 2018: 591-608 - [c33]Aina Niemetz
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255 - [c32]Dejan Jovanovic, Andrew Reynolds:
The FMCAD 2018 Graduate Student Forum. FMCAD 2018: 1 - [c31]Andrew Reynolds, Haniel Barbosa
Revisiting Enumerative Instantiation. TACAS (2) 2018: 112-131 - [i10]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR abs/1804.05025 (2018) - [i9]Clark W. Barrett, Haniel Barbosa
CVC4 at the SMT Competition 2018. CoRR abs/1806.08775 (2018) - 2017
- [j5]Andrew Reynolds, Tim King, Viktor Kuncak:
Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51(3): 500-532 (2017) - [j4]Andrew Reynolds, Jasmin Christian Blanchette
A Decision Procedure for (Co)datatypes in SMT Solvers. J. Autom. Reason. 58(3): 341-362 (2017) - [j3]Andrew Reynolds, Cesare Tinelli
Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. 17(4): 516-558 (2017) - [c30]Andrew Reynolds:
Challenges for Fast Synthesis Procedures in SMT. ARCADE@CADE 2017: 69-75 - [c29]Baoluo Meng
Relational Constraint Solving in SMT. CADE 2017: 148-165 - [c28]Burak Ekici
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. CAV (2) 2017: 126-133 - [c27]Andrew Reynolds, Maverick Woo, Clark W. Barrett
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. CAV (2) 2017: 453-474 - [c26]Andrew Reynolds, Cesare Tinelli
Designing Theory Solvers with Extensions. FroCoS 2017: 22-40 - [c25]Andrew Reynolds:
Quantifier Instantiation Beyond E-Matching. SMT 2017: 2 - [c24]Haniel Barbosa
Congruence Closure with Free Variables. TACAS (2) 2017: 214-230 - [c23]Andrew Reynolds, Radu Iosif, Cristina Serban:
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. VMCAI 2017: 462-482 - [c22]Andrew Reynolds, Cesare Tinelli:
SyGuS Techniques in the Core of an SMT Solver. SYNT@CAV 2017: 81-96 - [i8]Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli:
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. CoRR abs/1702.06259 (2017) - [i7]Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Constraint Solving for Finite Model Finding in SMT Solvers. CoRR abs/1706.00096 (2017) - 2016
- [j2]Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli
An efficient SMT solver for string constraints. Formal Methods Syst. Des. 48(3): 206-234 (2016) - [c21]Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King:
A Decision Procedure for Separation Logic in SMT. ATVA 2016: 244-261 - [c20]Andrew Reynolds:
Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. Vampire@IJCAR 2016: 1-15 - [c19]Kshitij Bansal, Andrew Reynolds, Clark W. Barrett
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR 2016: 82-98 - [c18]Andrew Reynolds, Jasmin Christian Blanchette
Model Finding for Recursive Functions in SMT. IJCAR 2016: 133-151 - [c17]Guy Katz, Clark W. Barrett
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD 2016: 93-100 - [c16]Clark W. Barrett
Efficient solving of string constraints for security analysis. HotSoS 2016: 4-6 - [c15]Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI 2016: 4205-4209 - [c14]Burak Ekici
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). HaTT@IJCAR 2016: 21-29 - [i6]Andrew Reynolds, Radu Iosif, Tim King:
A Decision Procedure for Separation Logic in SMT. CoRR abs/1603.06844 (2016) - [i5]Andrew Reynolds, Radu Iosif, Cristina Serban:
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic. CoRR abs/1610.04707 (2016) - 2015
- [c13]Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. CADE 2015: 197-213 - [c12]Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett
Deciding Local Theory Extensions via E-matching. CAV (2) 2015: 87-105 - [c11]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) 2015: 198-216 - [c10]Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCos 2015: 135-150 - [c9]Liana Hadarean, Clark W. Barrett
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. LPAR 2015: 340-355 - [c8]Andrew Reynolds, Viktor Kuncak:
Induction for SMT Solvers. VMCAI 2015: 80-98 - [i4]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli:
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR abs/1502.04464 (2015) - [i3]Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies:
On Deciding Local Theory Extensions via E-matching. CoRR abs/1508.06827 (2015) - [i2]Andrew Reynolds, Tim King, Viktor Kuncak:
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic. CoRR abs/1510.02642 (2015) - 2014
- [c7]Tianyi Liang, Andrew Reynolds, Cesare Tinelli
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. CAV 2014: 646-662 - [c6]Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli
A tour of CVC4: How it works, and how to use it. FMCAD 2014: 7 - [c5]Andrew Reynolds, Cesare Tinelli
Finding conflicting instances of quantified formulas in SMT. FMCAD 2014: 195-202 - [i1]Andrew Reynolds:
Approaches for Synthesis Conjectures in an SMT Solver. CoRR abs/1411.3970 (2014) - 2013
- [j1]Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli
SMT proof checking using a logical framework. Formal Methods Syst. Des. 42(1): 91-118 (2013) - [c4]Andrew Reynolds, Cesare Tinelli
Quantifier Instantiation Techniques for Finite Model Finding in SMT. CADE 2013: 377-391 - [c3]Andrew Reynolds, Cesare Tinelli
Finite Model Finding in SMT. CAV 2013: 640-655 - 2012
- [c2]Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang:
LFSC for SMT Proofs: Work in Progress. PxTP 2012: 21-27 - 2011
- [c1]Clark W. Barrett
CVC4. CAV 2011: 171-177
Coauthor Index
[c66] [c65] [c64] [i21] [j13] [j12] [j11] [j10] [c63] [c62] [c61] [c59] [i19] [c58] [c57] [c56] [c55] [c54] [c53] [c51] [i17] [j9] [j8] [c50] [c47] [d1] [i16] [i15] [c45] [c43] [j7] [c42] [c41] [c40] [c39] [c38] [c36] [i12] [i11] [j6] [c34] [c33] [i10] [i9] [j3] [c29] [c28] [c27] [c26] [i8] [i7] [j2] [c19] [c17] [c16] [c12] [c11] [c10] [c9] [i4] [i3] [c7] [c6] [c4] [c1]
[c66] [c65] [c64] [i21] [j13] [j12] [j11] [j10] [c63] [c62] [c61] [c59] [i19] [c58] [c57] [c56] [c55] [c54] [c53] [c51] [i17] [j9] [j8] [c50] [c47] [d1] [i16] [c46] [c45] [c44] [c43] [j7] [c42] [c41] [c40] [c39] [c38] [c37] [c36] [i12] [i11] [j6] [c34] [c33] [i10] [i9] [j3] [c29] [c28] [c27] [c26] [c22] [i8] [i7] [j2] [c19] [c18] [c17] [c16] [c14] [c11] [c10] [c9] [i4] [c7] [c6] [c5] [j1] [c4] [c3] [c2] [c1]
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-01 20:43 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: