SMT 2021
Satisfiability Modulo Theories 2021

Table of Contents

• Preface
  Summary: There were 16 papers submitted for peer-review to this workshop: 11 as presentation-only paper, 5 as extended abstract and 2 original papers. Out of these, 6 papers are published in this volume, 2 as regular papers and 4 as extended abstracts. Also included in this volume are abstracts for the 2 invited talks given at the workshop, and the abstracts of 2 papers that were submitted for presentation only. For the remaining presentation-only papers, we provide the references below.

Invited Talks

• Invited Talk: Using SMT and Abstraction-Refinement for Neural Network Verification 1
  Guy Katz
• Invited Talk: AVR: Word-Level Verification by Equality Abstraction of Data State 2
  Karem A. Sakallah

Extended Abstracts

• Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality 3-16
  Elisabeth Henkel , Jochen Hoenicke , Tanja Schindler
• First-Order Instantiation using Discriminating Terms 17-22
  Chad Brown , Mikoláš Janota
• Further Steps Down The Wrong Path: Improving the Bit-Blasting of Multiplication 23-31
  Martin Brain
• Dolmen: A Validator for SMT-LIB and Much More 32-39
  Guillaume Bury

Regular Papers

• AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff 40-52
  Jose Abel Castellanos Joo , Silvio Ghilardi , Alessandro Gianola , Deepak Kapur
• Characteristic Subsets of SMT-LIB Benchmarks 53-63
  Jan Jakubův , Mikoláš Janota , Andrew Reynolds

Presentation-Only Papers (Abstracts)

• Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant 64
  Hans-Jörg Schurr , Mathias Fleury , Martin Desharnais
• Abstract: The Extended Theory of Trees and Algebraic (Co)datatypes 65
  Fabian Zaiser , Luke Ong

Presentation-Only Papers (References)

• Politeness and Stable Infiniteness: Stronger Together (paper published at CADE 2021 , available here )
  Ying Sheng , Yoni Zohar , Christophe Ringeissen , Andrew Reynolds , Clark Barrett , Cesare Tinelli
• Quantifier Simplification by Unification in SMT (paper to appear at FROCOS 2021 )
  Hans-Jörg Schurr , Pascal Fontaine
• On Symmetry and Quantification: A New Approach to Verify Distributed Protocols (paper published at NFM 2021 , available here )
  Aman Goel , Karem A. Sakallah
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (paper published at TACAS 2021 , available here )
  Makai Mann , Ahmed Irfan , Alberto Griggio , Oded Padon , Clark Barrett
• Theory-Specific Proof Steps Witnessing Correctness of SMT Executions (paper to appear at DAC 2021 , available here )
  Rodrigo Otoni , Martin Blicha , Patrick Eugster , Antti E. J. Hyvärinen , Natasha Sharygina
• Smt-Switch: A Solver-agnostic C++ API for SMT Solving (paper published at SAT 2021 )
  Makai Mann , Amalee Wilson , Yoni Zohar , Lindsey Stuntz , Ahmed Irfan , Kristopher Brown , Caleb Donovick , Allison Guman , Cesare Tinelli , Clark Barrett