Andrew Reynolds

113 papers A* 4A 14B 24Journal 37Unranked 33
YearRankTypeTitle / Venue / Authors
2026 — conf
Enumerating Choice Terms in Model-Based Quantifier Instantiation.
TACAS (1)
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, Cesare Tinelli
2026 B conf
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions.
CPP
Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2025 — conf
Augmenting Model-Based Instantiation with Fast Enumeration.
TACAS (1)
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette
2025 A conf
Bit-Precise Reasoning with Parametric Bit-Vectors.
SAT
Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2025 B conf
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL.
ITP
Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli
2025 J jnl
Lean-SMT: An SMT tactic for discharging proof goals in Lean.
CoRR
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2025 B conf
Solving Set Constraints with Comprehensions and Bounded Quantifiers.
FMCAD
Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik
2025 J jnl
Solving Set Constraints with Comprehensions and Bounded Quantifiers.
CoRR
Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik
2025 B conf
Towards SMT Solver Stability via Input Normalization.
FMCAD
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett
2025 — conf
lean-smt: An SMT Tactic for Discharging Proof Goals in Lean.
CAV (3)
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2024 — conf
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.
TACAS (1)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2024 B conf
SMT-D: New Strategies for Portfolio-Based SMT Solving.
FMCAD
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 — conf
Satisfiability Modulo Theories: A Beginner's Tutorial.
FM (2)
Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar
2024 — conf
The SemGuS Toolkit.
CAV (3)
Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni
2024 J jnl
The SemGuS Toolkit.
CoRR
Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni
2024 J jnl
Using Normalization to Improve SMT Solver Stability.
CoRR
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett
2024 — ed.
Verified Software. Theories, Tools and Experiments - 15th International Conference, VSTTE 2023, Ames, IA, USA, October 23-24, 2023, Revised Selected Papers
VSTTE
Andrew Reynolds, Serdar Tasiran
2024 J jnl
Verifying SQL Queries using Theories of Tables and Relations.
CoRR
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2024 B conf
Verifying SQL queries using theories of tables and relations.
LPAR
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2023 B conf
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery.
FMCAD
Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2023 B conf
An Interactive SMT Tactic in Coq using Abductive Reasoning.
LPAR
Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
2023 — conf
Automatic Verification of SMT Rewrites in Isabelle/HOL.
SMT
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2023 J jnl
Combining Stable Infiniteness and (Strong) Politeness.
J. Autom. Reason.
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2023 J jnl
Generating and Exploiting Automated Reasoning Proof Certificates.
Commun. ACM
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
2023 B conf
Partitioning Strategies for Distributed SMT Solving.
FMCAD
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
2023 J jnl
Partitioning Strategies for Distributed SMT Solving.
CoRR
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
2023 J jnl
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences.
J. Autom. Reason.
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2023 — conf
Selecting Quantifiers for Instantiation in SMT.
SMT
Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds
2023 J jnl
Synthesising Programs with Non-trivial Constants.
J. Autom. Reason.
Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
2023 J jnl
The SyGuS Language Standard Version 2.1.
CoRR
Saswat Padhi, Elizabeth Polgreen, Mukund Raghothaman, Andrew Reynolds, Abhishek Udupa
2022 B conf
Bit-Precise Reasoning via Int-Blasting.
VMCAI
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022 A conf
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description).
IJCAR
Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022 — conf
Even Faster Conflicts and Lazier Reductions for String Solvers.
CAV (2)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2022 A conf
Flexible Proof Production in an Industrial-Strength SMT Solver.
IJCAR
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
2022 A conf
Reasoning About Vectors Using an SMT Theory of Sequences.
IJCAR
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022 J jnl
Reasoning About Vectors using an SMT Theory of Sequences.
CoRR
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022 B conf
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.
FMCAD
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022 B conf
Satisfiability and Synthesis Modulo Oracles.
VMCAI
Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
2022 — conf
cvc5: A Versatile and Industrial-Strength SMT Solver.
TACAS (1)
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
2021 — conf
Characteristic Subsets of SMT-LIB Benchmarks.
SMT
Jan Jakubuv, Mikolás Janota, Andrew Reynolds
2021 B conf
Fair and Adventurous Enumeration of Quantifier Instantiations.
FMCAD
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021 J jnl
Fair and Adventurous Enumeration of Quantifier Instantiations.
CoRR
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021 J jnl
On solving quantified bit-vector constraints using invertibility conditions.
Formal Methods Syst. Des.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021 A conf
Politeness and Stable Infiniteness: Stronger Together.
CADE
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021 J jnl
Politeness and Stable Infiniteness: Stronger Together.
CoRR
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021 J jnl
Satisfiability and Synthesis Modulo Oracles.
CoRR
Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
2021 — conf
Syntax-Guided Quantifier Instantiation.
TACAS (2)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021 J jnl
Towards Satisfiability Modulo Parametric Bit-vectors.
J. Autom. Reason.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2021 J jnl
lazybvtoint at the SMT Competition 2020.
CoRR
Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett
2020 — conf
A Decision Procedure for String to Code Point Conversion.
IJCAR (1)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2020 B conf
Reductions for Strings and Regular Expressions Revisited.
FMCAD
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2020 B conf
SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces.
FMCAD
M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli
2020 — conf
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis.
IJCAR (1)
Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
2019 J jnl
CVC4SY for SyGuS-COMP 2019.
CoRR
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2019 A conf
Extending SMT Solvers to Higher-Order Logic.
CADE
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett
2019 B conf
Extending enumerative function synthesis via SMT-driven classification.
FMCAD
Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli
2019 — conf
High-Level Abstractions for Simplifying Extended String Constraints in SMT.
CAV (2)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2019 — conf
Invertibility Conditions for Floating-Point Formulas.
CAV (2)
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2019 J jnl
Refutation-based synthesis in SMT.
Formal Methods Syst. Des.
Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2019 — conf
SL-COMP: Competition of Solvers for Separation Logic.
TACAS (3)
Mihaela Sighireanu, Juan Antonio Navarro Pérez, 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, Tomás Vojnar, Constantin Enea, Ondrej Lengál, Chong Gao, Zhilin Wu
2019 A conf
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.
SAT
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
2019 A conf
Towards Bit-Width-Independent Proofs in SMT Solvers.
CADE
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019 J jnl
Towards Bit-Width-Independent Proofs in SMT Solvers.
CoRR
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019 — conf
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis.
CAV (2)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2018 J jnl
CVC4 at the SMT Competition 2018.
CoRR
Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
2018 A conf
Datatypes with Shared Selectors.
IJCAR
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett
2018 J jnl
On Solving Quantified Bit-Vectors using Invertibility Conditions.
CoRR
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2018 J jnl
Reasoning with Finite Sets and Cardinality Constraints in SMT.
Log. Methods Comput. Sci.
Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
2018 — conf
Revisiting Enumerative Instantiation.
TACAS (2)
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
2018 — conf
Solving Quantified Bit-Vectors Using Invertibility Conditions.
CAV (2)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2018 B conf
The FMCAD 2018 Graduate Student Forum.
FMCAD
Dejan Jovanovic, Andrew Reynolds
2017 J jnl
A Decision Procedure for (Co)datatypes in SMT Solvers.
J. Autom. Reason.
Andrew Reynolds, Jasmin Christian Blanchette
2017 J jnl
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT.
CoRR
Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
2017 — conf
Challenges for Fast Synthesis Procedures in SMT.
ARCADE@CADE
Andrew Reynolds
2017 — conf
Congruence Closure with Free Variables.
TACAS (2)
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2017 J jnl
Constraint Solving for Finite Model Finding in SMT Solvers.
CoRR
Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017 J jnl
Constraint solving for finite model finding in SMT solvers.
Theory Pract. Log. Program.
Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017 — conf
Designing Theory Solvers with Extensions.
FroCoS
Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett
2017 — conf
Quantifier Instantiation Beyond E-Matching.
SMT
Andrew Reynolds
2017 B conf
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic.
VMCAI
Andrew Reynolds, Radu Iosif, Cristina Serban
2017 A conf
Relational Constraint Solving in SMT.
CADE
Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017 — conf
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.
CAV (2)
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett
2017 — conf
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification.
CAV (2)
Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli
2017 J jnl
Solving quantified linear arithmetic by counterexample-guided instantiation.
Formal Methods Syst. Des.
Andrew Reynolds, Tim King, Viktor Kuncak
2017 — conf
SyGuS Techniques in the Core of an SMT Solver.
SYNT@CAV
Andrew Reynolds, Cesare Tinelli
2016 A* conf
A Decision Procedure for (Co)datatypes in SMT Solvers.
IJCAI
Andrew Reynolds, Jasmin Christian Blanchette
2016 B conf
A Decision Procedure for Separation Logic in SMT.
ATVA
Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King
2016 J jnl
A Decision Procedure for Separation Logic in SMT.
CoRR
Andrew Reynolds, Radu Iosif, Tim King
2016 A conf
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT.
IJCAR
Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2016 J jnl
An efficient SMT solver for string constraints.
Formal Methods Syst. Des.
Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2016 — conf
Conflicts, Models and Heuristics for Quantifier Instantiation in SMT.
Vampire@IJCAR
Andrew Reynolds
2016 — conf
Efficient solving of string constraints for security analysis.
HotSoS
Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze
2016 B conf
Lazy proofs for DPLL(T)-based SMT solvers.
FMCAD
Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean
2016 A conf
Model Finding for Recursive Functions in SMT.
IJCAR
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
2016 J jnl
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic.
CoRR
Andrew Reynolds, Radu Iosif, Cristina Serban
2015 A conf
A Decision Procedure for (Co)datatypes in SMT Solvers.
CADE
Andrew Reynolds, Jasmin Christian Blanchette
2015 — conf
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings.
FroCos
Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2015 J jnl
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic.
CoRR
Andrew Reynolds, Tim King, Viktor Kuncak
2015 — conf
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.
CAV (2)
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett
2015 — conf
Deciding Local Theory Extensions via E-matching.
CAV (2)
Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies
2015 B conf
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors.
LPAR
Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters
2015 B conf
Induction for SMT Solvers.
VMCAI
Andrew Reynolds, Viktor Kuncak
2015 J jnl
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4.
CoRR
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli
2015 J jnl
On Deciding Local Theory Extensions via E-matching.
CoRR
Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies
2014 A* conf
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.
CAV
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2014 B conf
A tour of CVC4: How it works, and how to use it.
FMCAD
Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli
2014 J jnl
Approaches for Synthesis Conjectures in an SMT Solver.
CoRR
Andrew Reynolds
2014 B conf
Finding conflicting instances of quantified formulas in SMT.
FMCAD
Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura
2013 A* conf
Finite Model Finding in SMT.
CAV
Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic
2013 A conf
Quantifier Instantiation Techniques for Finite Model Finding in SMT.
CADE
Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett
2013 J jnl
SMT proof checking using a logical framework.
Formal Methods Syst. Des.
Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli
2012 — conf
LFSC for SMT Proofs: Work in Progress.
PxTP
Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang
2011 A* conf
CVC4.
CAV
Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli