Andrew Reynolds

From MaRDI portal
Person:518398

Available identifiers

zbMath Open reynolds.andrewMaRDI QIDQ518398

List of research outcomes

PublicationDate of PublicationType
High-level abstractions for simplifying extended string constraints in SMT2024-02-16Paper
Invertibility conditions for floating-point formulas2024-02-16Paper
Reasoning about vectors: satisfiability modulo a theory of sequences2023-10-24Paper
Combining stable infiniteness and (strong) politeness2023-10-24Paper
Synthesising programs with non-trivial constants2023-06-27Paper
Solving quantified bit-vectors using invertibility conditions2023-05-05Paper
Flexible proof production in an industrial-strength SMT solver2022-12-07Paper
Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)2022-12-07Paper
Reasoning about vectors using an SMT theory of sequences2022-12-07Paper
Even Faster Conflicts and Lazier Reductions for String Solvers2022-12-07Paper
Scalable algorithms for abduction via enumerative syntax-guided synthesis2022-11-09Paper
A decision procedure for string to code point conversion2022-11-09Paper
SMTCoq: a plug-in for integrating SMT solvers into Coq2022-08-12Paper
Scaling up DPLL(T) string solvers using context-dependent simplification2022-08-12Paper
Satisfiability and synthesis modulo oracles2022-07-08Paper
Politeness and stable infiniteness: stronger together2021-12-01Paper
Towards satisfiability modulo parametric bit-vectors2021-11-24Paper
Syntax-guided quantifier instantiation2021-10-18Paper
On solving quantified bit-vector constraints using invertibility conditions2021-08-30Paper
Congruence Closure with Free Variables2020-08-05Paper
Syntax-guided rewrite rule enumeration for SMT solvers2020-05-20Paper
Extending SMT solvers to higher-order logic2020-03-10Paper
Towards bit-width-independent proofs in SMT solvers2020-03-10Paper
Refutation-based synthesis in SMT2019-12-18Paper
Revisiting enumerative instantiation2019-09-16Paper
https://portal.mardi4nfdi.de/entity/Q45532832018-11-02Paper
A decision procedure for separation logic in SMT2018-10-25Paper
Datatypes with shared selectors2018-10-18Paper
Deciding local theory extensions via E-matching2018-03-01Paper
Counterexample-guided quantifier instantiation for synthesis in SMT2018-03-01Paper
Solving quantified linear arithmetic by counterexample-guided instantiation2018-01-08Paper
Designing theory solvers with extensions2018-01-04Paper
Constraint solving for finite model finding in SMT solvers2017-11-09Paper
Relational constraint solving in SMT2017-09-22Paper
A decision procedure for (co)datatypes in SMT solvers2017-06-29Paper
An efficient SMT solver for string constraints2017-03-28Paper
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings2017-02-27Paper
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic2017-02-21Paper
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT2016-09-05Paper
Model Finding for Recursive Functions in SMT2016-09-05Paper
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors2016-01-12Paper
A Decision Procedure for (Co)datatypes in SMT Solvers2015-12-02Paper
Induction for SMT Solvers2015-02-04Paper
SMT proof checking using a logical framework2014-03-28Paper
Quantifier Instantiation Techniques for Finite Model Finding in SMT2013-06-14Paper
https://portal.mardi4nfdi.de/entity/Q45521402002-08-29Paper

Research outcomes over time


Doctoral students

No records found.


Known relations from the MaRDI Knowledge Graph

PropertyValue
MaRDI profile typeMaRDI person profile
instance ofhuman


This page was built for person: Andrew Reynolds