=Paper=
{{Paper
|id=Vol-3725/preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-3725/preface.pdf
|volume=Vol-3725
}}
==None==
https://ceur-ws.org/Vol-3725/preface.pdf
Satisfiability Modulo Theories
22nd International Workshop
SMT 2024
Proceedings
Montreal, Canada
Affiliated with CAV-36
July 22 – 23, 2024
Giles Reger1 , Yoni Zohar2
1
Amazon Web Services (AWS)
2
Bar Ilan University
SMT 2024: 22st International Workshop on Satisfiability Modulo Theories July 22–23, 2024, Montreal Canada
$ reggiles@amazon.com (G. Reger); yoni.zohar@biu.ac.il (Y. Zohar)
http://www.cs.man.ac.uk/~regerg/ (G. Reger); https://u.cs.biu.ac.il/~zoharyo1/ (Y. Zohar)
© 2024 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).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
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 (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 efforts.
The aim of the workshop is to bring together researchers and users of SMT tools and tech-
niques. 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
Program Committee
Program Chairs
Giles Reger, AWS
Yoni Zohar, Bar Ilan University
Program Committee
Katalin Fazekas, TU Wien
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
Subreviewers
Enrico Lipparini, University of Genoa
Thomas Hader, TU Wien
Contents
Invited Talks
The Hows and Whys of Higher-Order SMT . . . . . . . . . . . . . . . . . . . . . . . 1
Sophie Tourret,
Challenges in Bit-Vector Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
Mathias Preiner
Regular Papers
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
Extended Abstracts
CSB: A Counting and Sampling tool for Bit-vectors . . . . . . . . . . . . . . . . . . 36
Arijit Shaw and Kuldeep S. Meel
Minimal logic detection and exporting smtlib problems with Dolmen . . . . . . . . 44
Guillaume Bury
A Bit-vector to Integer Translation with bv2nat and nat2bv . . . . . . . . . . . . . . 53
Max Barth and Matthias Heizmann
An SMT theory for N-Indexed Sequences . . . . . . . . . . . . . . . . . . . . . . . . 64
Hichem Rami Ait El Hara, François Bobot and Guillaume Bury
Presentation-Only Papers (Abstracts)
Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis . . . . . . 75
Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel Day, Florin Manea and Vijay Ganesh