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
A grouping.
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.
5 references
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