Andrew Reynolds

5 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.

This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

Andrew Reynolds

Getting an SMT solver to decide things: a decision procedure for separation logic in SMT, the Bernays-Schönfinkel-Ramsey fragment of it, and the SL-COMP benchmark the solvers are measured in, over general quantifier-instantiation technique. The shape is the reverse of most people in the separation-logic set -- the logic is an application of the solver work rather than the other way round. Not to be confused with John C. Reynolds, who has a page of his own here and also appears in separation-logic a decade and a half earlier; only the given name separates them in an author list.

Syntax-Guided Quantifier Instantiation
Aina Niemetz and others (2021) · 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems · Springer
SL-COMP: Competition of Solvers for Separation Logic
Mihaela Sighireanu and others (2019) · International Conference on Tools and Algorithms for the Construction and Analysis of Systems · Springer
Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic
Andrew Reynolds and others (2017) · 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) · Springer
Solving quantified linear arithmetic by counterexample-guided instantiation
Andrew Reynolds and others (2017) · Formal Methods in System Design
A Decision Procedure for Separation Logic in SMT
Andrew Reynolds and others (2016) · Automated Technology for Verification and Analysis · Springer