Andrew Reynolds
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
71
Venues
14
Active years
2011–2026
Best venue rank
A*
Where they publish
Papers
71 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver. | Andrew Reynolds, Hans-Jrg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett, Cesare Tinelli |
| 2026 | CPP | Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. | Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | IJCAR | Checking Regular Expressions in Cvc5 Proofs. | Ofec Israel, Yoni Zohar, Andrew Reynolds, S. Hitarth, Bruno Dutertre, Clark W. Barrett, Cesare Tinelli |
| 2026 | IJCAR | A General Approach for SMT Proof Skeletons. | Joseph E. Reeves, Haniel Barbosa, Andrew Reynolds, Marijn J. H. Heule |
| 2026 | IJCAR | Ethos: A Fast Proof Checker for the Eunoia Logical Framework. | Andrew Reynolds, Hans-Jrg Schurr, Mallku Soldevila, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | TACAS | Enumerating Choice Terms in Model-Based Quantifier Instantiation. | Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, Cesare Tinelli |
| 2025 | CAV | lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. | Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett |
| 2025 | FMCAD | Towards SMT Solver Stability via Input Normalization. | Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett |
| 2025 | FMCAD | Solving Set Constraints with Comprehensions and Bounded Quantifiers. | Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik |
| 2025 | ITP | Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jrg Schurr, Clark W. Barrett, Cesare Tinelli |
| 2025 | SAT | Bit-Precise Reasoning with Parametric Bit-Vectors. | Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2025 | TACAS | Augmenting Model-Based Instantiation with Fast Enumeration. | Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette |
| 2024 | CAV | The SemGuS Toolkit. | Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni |
| 2024 | FM | Satisfiability Modulo Theories: A Beginner's Tutorial. | Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar |
| 2024 | FMCAD | SMT-D: New Strategies for Portfolio-Based SMT Solving. | Clark W. Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert B. Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Christopher Stephens, Michael W. Whalen |
| 2024 | LPAR | Verifying SQL queries using theories of tables and relations. | Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett |
| 2024 | TACAS | IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2023 | FMCAD | A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. | Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2023 | FMCAD | Partitioning Strategies for Distributed SMT Solving. | Amalee Wilson, Andres Ntzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett |
| 2023 | LPAR | An Interactive SMT Tactic in Coq using Abductive Reasoning. | Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Flexible Proof Production in an Industrial-Strength SMT Solver. | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). | Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | CADE | Reasoning About Vectors Using an SMT Theory of Sequences. | Ying Sheng, Andres Ntzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli |
| 2022 | CAV | Even Faster Conflicts and Lazier Reductions for String Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2022 | FMCAD | Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. | Andres Ntzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | TACAS | cvc5: A Versatile and Industrial-Strength SMT Solver. | Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar |
| 2022 | VMCAI | Satisfiability and Synthesis Modulo Oracles. | Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia |
| 2022 | VMCAI | Bit-Precise Reasoning via Int-Blasting. | Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Ntzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | CADE | Politeness and Stable Infiniteness: Stronger Together. | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | FMCAD | Fair and Adventurous Enumeration of Quantifier Instantiations. | Mikols Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds |
| 2021 | TACAS | Syntax-Guided Quantifier Instantiation. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2020 | CADE | Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli |
| 2020 | CADE | A Decision Procedure for String to Code Point Conversion. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2020 | FMCAD | SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. | M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli |
| 2020 | FMCAD | Reductions for Strings and Regular Expressions Revisited. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | CADE | Extending SMT Solvers to Higher-Order Logic. | Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett |
| 2019 | CADE | Towards Bit-Width-Independent Proofs in SMT Solvers. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | Invertibility Conditions for Floating-Point Formulas. | Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | High-Level Abstractions for Simplifying Extended String Constraints in SMT. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | FMCAD | Extending enumerative function synthesis via SMT-driven classification. | Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli |
| 2019 | SAT | Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli |
| 2019 | TACAS | SL-COMP: Competition of Solvers for Separation Logic. | Mihaela Sighireanu, Juan Antonio Navarro Prez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Toms Vojnar, Constantin Enea, Ondrej Lengl, Chong Gao, Zhilin Wu |
| 2018 | CADE | Datatypes with Shared Selectors. | Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett |
| 2018 | CAV | Solving Quantified Bit-Vectors Using Invertibility Conditions. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2018 | FMCAD | The FMCAD 2018 Graduate Student Forum. | Dejan Jovanovic, Andrew Reynolds |
| 2018 | TACAS | Revisiting Enumerative Instantiation. | Andrew Reynolds, Haniel Barbosa, Pascal Fontaine |
| 2017 | CADE | Relational Constraint Solving in SMT. | Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett |
| 2017 | CADE | Challenges for Fast Synthesis Procedures in SMT. | Andrew Reynolds |
| 2017 | CAV | SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. | Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett |
| 2017 | CAV | Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. | Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli |
| 2017 | TACAS | Congruence Closure with Free Variables. | Haniel Barbosa, Pascal Fontaine, Andrew Reynolds |
| 2017 | VMCAI | Reasoning in the Bernays-Schnfinkel-Ramsey Fragment of Separation Logic. | Andrew Reynolds, Radu Iosif, Cristina Serban |
| 2016 | ATVA | A Decision Procedure for Separation Logic in SMT. | Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King |
| 2016 | CADE | A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. | Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2016 | CADE | Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. | Andrew Reynolds |
| 2016 | CADE | Model Finding for Recursive Functions in SMT. | Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli |
| 2016 | FMCAD | Lazy proofs for DPLL(T)-based SMT solvers. | Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean |
| 2016 | IJCAI | A Decision Procedure for (Co)datatypes in SMT Solvers. | Andrew Reynolds, Jasmin Christian Blanchette |
| 2015 | CADE | A Decision Procedure for (Co)datatypes in SMT Solvers. | Andrew Reynolds, Jasmin Christian Blanchette |
| 2015 | CAV | Deciding Local Theory Extensions via E-matching. | Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies |
| 2015 | CAV | Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. | Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett |
| 2015 | LPAR | Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. | Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters |
| 2015 | VMCAI | Induction for SMT Solvers. | Andrew Reynolds, Viktor Kuncak |
| 2014 | CAV | A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. | Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters |
| 2014 | FMCAD | A tour of CVC4: How it works, and how to use it. | Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli |
| 2014 | FMCAD | Finding conflicting instances of quantified formulas in SMT. | Andrew Reynolds, Cesare Tinelli, Leonardo Mendona de Moura |
| 2013 | CADE | Quantifier Instantiation Techniques for Finite Model Finding in SMT. | Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett |
| 2013 | CAV | Finite Model Finding in SMT. | Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic |
| 2011 | CAV | CVC4. | Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli |
| 2011 | MOBICOM | The commotion wireless project. | Andrew Reynolds, Josh King, Sascha D. Meinrath, Thomas Gideon |