The 22nd International Workshop on Satisfiability Modulo Theories was held in Montreal, Canada, on July 22nd and 23rd in association with the International Conference on Computer Aided Verification (CAV-36).
The SMT workshop is an annual event dedicated to Satisfiability Modulo Theories (SMT).
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 2024 featured invited talks by Sophie Tourret from INRIA and Mathias Preiner from Stanford University, and the presentation of 12 peer-reviewed papers. The workshop received 13 submissions, out of which 12 were accepted. Each submission was reviewed by three program committee members. Of the 12 accepted submissions, seven are published in this volume: three as original papers, and four as extended abstracts. The remaining five were submitted to the workshop for presentation only. For one of them, the authors include the paper abstract in this volume.
We would like to thank the program committee, the subreviewers, the authors, the invited speakers, the SMT-COMP organizers, workshop participants and the SMT Steering Committee for their contribution to the workshop. We would further like to thank the CAV organizers for hosting the workshop, EasyChair for the availability of their conference system, and CEUR for their help to publish these proceedings.
SMT 2024 was sponsored by AWS, Halmos, and Ethereum Foundation. We are grateful for their generosity in supporting the workshop.
Program Committee
Yoni Zohar, Bar Ilan University
Viktor Kuncak, Ecole Polytechnique Fédérale de Lausanne Ahmed Irfan, SRI International Aina Niemetz, Stanford University Andrew Reynolds, University of Iowa Daniela Kaufmann, TU Wien Haniel Barbosa, Universidade Federal de Minas Gerais Nadia Labai, Amazon Clark Barrett, Stanford University Alexander Nadel, Technion and Intel Philipp Rümmer, University of Regensburg Nestan Tsiskaridze, Stanford University Guilherme Toledo, Bar Ilan University Yannick Moy, AdaCore Martin Suda, Czech Technical University in Prague Stéphane Graham-Lengrand, SRI International François Bobot, CEA Mate Soos, Ethereum Foundation Nikolaj Bjørner, Microsoft
Thomas Hader, TU Wien
The Hows and Whys of Higher-Order SMT . . . . . . . . . . . . . . . . . . . . . . . 1
Sophie Tourret, Challenges in Bit-Vector Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
Mathias Preiner An SMT-LIB Theory of Finite Fields . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
Thomas Hader and Alex Ozdemir Reconstruction of SMT proofs with Lambdapi . . . . . . . . . . . . . . . . . . . . . 13
Alessio Coltellacci, Stephan Merz and Gilles Dowek Arrays Reasoning in MCSat . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
Ahmed Irfan and Stephane Graham-Lengrand