A Proposal for an OMT Extension to SMT-LIB

Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli and Clark Barrett

An Interactive SMT Tactic in Coq Using Abductive Reasoning

Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli and Clark Barrett

Reasoning About Vectors Using an SMT Theory of Sequences

Ying Sheng, Andres Noetzli, Andrew Reynolds, Yoni Zohar, David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett and Cesare Tinelli

Invited Talk: From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT

Andrew Reynolds and Cesare Tinelli

Extending SMT solvers to Higher-Order Logic

Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett

Towards Bit Width Independent Proofs in SMT Solvers

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett and Cesare Tinelli

Counterexample-Guided Quantifier Instantiation in Logical Theories

Andrew Reynolds and Cesare Tinelli

Towards Enumerative Invariant Synthesis in SMT Solvers

Andrew Reynolds

Higher-Order SMT Solving

Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui and Cesare Tinelli

Revisiting Enumerative Instantiation

Andrew Reynolds, Haniel Barbosa and Pascal Fontaine

Solving Quantified Bit-Vectors using Invertibility Conditions

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli

Datatypes with Shared Selectors

Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli and Clark Barrett

Rewrites for SMT Solvers using Syntax-Guided Enumeration

Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Noetzli, Mathias Preiner, Clark Barrett and Cesare Tinelli