(editors) SMT 2022: Satisfiability Modulo Theories, August 11–12, 2022, Haifa, Israel © 2022 Copyright for the individual papers by the papers’ authors. Copyright for the volume as a collection by its editors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0).
CPWrEooUrckResehdoinpgs IhStpN:/c1e6u1r3-w-0s.o7r3g CEUR Workshop Proceedings (CEUR-WS.org) The International Workshop on Satisfiability Modulo Theories is an annual event dedicated to Satisfiability Modulo Theories (SMT). The 20th edition of the SMT workshop was held in Haifa, Israel, on August 11th and 12th in association with the International Joint Conference on Automated Reasoning 2022 (IJCAR 2022), as part of the 8th Federated Logic Conference (FLoC 2022).
Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and combination methods that allow one to obtain more versatile SMT tools, usually leveraging Boolean satisfiability (SAT) solvers. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification eforts.
The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to: • Decision procedures and theories of interest • Combinations of decision procedures • Novel implementation techniques • Benchmarks and evaluation methodologies • Applications and case studies • Theoretical results
SMT 2022 featured an invited talk by Aina Niemetz from Stanford University, a panel discussion, and the presentation of 14 peer-reviewed papers, along with a discussion on SMT proofs and a competitive event. The workshop received 15 paper submissions, out of which 14 were accepted. Each submission was reviewed by three program committee members. Of the 14 accepted submissions, four were accepted as regular papers, and six as extended abstracts. The remaining five contributions were submitted to the workshop for presentation only. The authors of one of these presentations agreed to include the abstract of their talk into these proceedings.
We would like to thank the program committee, the subreviewers, the authors, the invited speaker, the panelists, the SMT competition organisers and participants, and the SMT Steering Committee for their contributions to the workshop. We thank Alexander Nadel and Aina Niemetz, the chairs of SMT 2021 for their valuable advice in organising the workshop. We would further like to thank the IJCAR and FLoC organizers for hosting the workshop, EasyChair for the availability of their conference system, and CEUR for their help to publish these proceedings.
SMT 2022 was sponsored by AdaCore, Ethereum Foundation, Informal Systems, and Runtime
David Déharbe, CLEARSY
Stéphane Graham-Lengrand, SRI International
Invited Talk: Local Search for Bit-Precise Reasoning and Beyond
Aina Niemetz
Trail Saving in SMT
Milan Banković, David Šćepanović A Simple Proof Format for SMT
Jochen Hoenicke, Tanja Schindler
CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract
Length
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar 38 54 71 80 90 99 114 128