SMT 2022
Satisfiability Modulo Theories 2022

Table of Contents

• Preface
  Summary: There were 15 contributions submitted for peer-review to this workshop, 4 as regular papers, 6 as extended abstracts, and 5 as presentation only. Out of these, 9 papers are published in these proceedings, 4 as regular papers, 5 as extended abstracts. Also included in this volume is the abstract for an invited talk and one abstract of a paper that was submitted as a presentation-only. For the remaining 4 presentation-only papers we provide the references.

Invited Talks

• Invited Talk: Local Search for Bit-Precise Reasoning and Beyond 1
  Aina Niemetz

Regular Papers

• Trail Saving in SMT 2-17
  Milan Banković, David Šćepanović
• CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length 18-37
  Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
• An SMT-LIB Theory of Heaps 38-53
  Zafer Esen, Philipp Rümmer
• A Simple Proof Format for SMT 54-70
  Jochen Hoenicke, Tanja Schindler

Extended Abstracts

• User-Propagators for Custom Theories in SMT Solving 71-79
  Nikolaj Bjørner, Clemens Eisenhofer, Laura Kovács
• The VMT-LIB Language and Tools 80-89
  Alessandro Cimatti, Alberto Griggio, Stefano Tonetta
• An SMT Approach for Solving Polynomials over Finite Fields 90-98
  Thomas Hader, Laura Kovács
• Goose: A Meta-Solver for Deep Neural Network Verification 99-113
  Joseph Scott, Guanting Pan, Elias B. Khalil, Vijay Ganesh
• On Satisfiability of Polynomial Equations over Large Prime Fields 114-127
  Lucas Clemente Vella, Leonardo Alt

Presentation-Only Papers (Abstracts)

• Abstract: Challenges and Solutions for Higher-Order SMT Proofs 128
  Chad E. Brown, Mikoláš Janota, Cezary Kaliszyk

Presentation-Only Papers (References)

• NORMA: A Tool for the Analysis of Relay-based Railway Interlocking Systems (paper published at TACAS 2022, available here)
  Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella, Marco Zamboni
• cvc5: A Versatile and Industrial-Strength SMT Solver (paper published at TACAS 2022, available here)
  Haniel Barbosa, Clark Barrett, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mahgoub, Yahia Mohammed, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
• Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (to appear in CAV 2022)
  Aina Niemetz, Mathias Preiner, Clark Barrett
• Bit-Precise Reasoning via Int-Blasting (paper published at VMCAI 2022, available here)
  Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Noetzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli