Preface

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 .

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 efforts.

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.

Giles Reger and Yoni Zohar Co-chairs, SMT 2024