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