SMT-LIB Report

Clark Barrett, Pascal Fontaine and Cesare Tinelli

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

Smt-Switch: a Solver-agnostic C++ API for SMT Solving

Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli and Clark Barrett

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

Contract-based Compositional Verification of Infinite-State Reactive Systems

Cesare Tinelli

Counterexample-Guided Quantifier Instantiation in Logical Theories

Andrew Reynolds and Cesare Tinelli

Higher-Order SMT Solving

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

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