The Coq mailing list

[geoff AT cs.miami.edu]

=======================================================================
SMT 2025: 23rd International Workshop on Satisfiability Modulo Theories
Glasgow, UK, August 10–11, 2025
Affiliated with SAT 2025
=======================================================================

Website: https://smt-workshop.cs.uiowa.edu/2025/
Submission deadline: May 14th, 2025

Background
----------
Determining the satisfiability of first-order formulas modulo background 
theories, known as the Satisfiability Modulo Theories (SMT) 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. These ingredients together make SMT 
techniques well-suited for use in larger automated reasoning and verification 
efforts.

Aim and Scope
-------------
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
- Applications and case studies
- Benchmarks and evaluation methodologies
- Theoretical results

Paper submission and Proceedings
--------------------------------
Three categories of submissions are invited:

- Extended abstracts : given the informal style of the workshop, we strongly 
encourage the submission of preliminary reports of work in progress. They may 
range in length from very short (a couple of pages) to 10 pages and they will 
be judged based on the expected level of interest for the SMT community. They 
will be included in the informal proceedings.
- Original papers: contain original research (simultaneous submissions are 
not allowed[*]) and sufficient detail to assess the merits and relevance of 
the submission. For papers reporting experimental results, authors are 
strongly encouraged to make their data available. Original papers should not 
exceed 12 pages (excluding references).
- Presentation-only papers: describe work recently published or submitted and 
will not be included in the proceedings. We see this as a way to provide 
additional access to important developments that SMT Workshop attendees may 
be unaware of. Presentation-only papers may be submitted as originally 
published, if published elsewhere, and should not exceed 12 pages otherwise.

Papers in all three categories will be peer-reviewed. All papers should be in 
standard-conforming PDF. Technical details may be included in an appendix to 
be read at the reviewers' discretion. Final versions should be prepared in 
LaTeX using the CEURART style file. The page limit does not include 
references. Proceedings shall be submitted to CEUR-WS.org for online 
publication.

[*] Due to deadline conflicts, we will allow resubmissions from SAT. They 
will be turned into presentation-only papers in case of acceptance at both 
SAT and SMT. The title of such submissions must include “(SAT 
resubmission)”.

Invited Speakers
----------------
TBA

Program Chairs
--------------
Jochen Hoenicke – Certora
Sophie Tourret – Inria

Program Committee
-----------------
Haniel Barbosa – Universidade Federal de Minas Gerais, Brazil
Nikolaj Bjørner        – Microsoft, US
Maria Paola Bonacina – Università degli Studi di Verona, Italy
Guillaume Bury – OCamlPro, France
Bruno Dutertre – Amazon Web Services, US
Katalin Fazekas – TU Wien, Austria
Pascal Fontaine – Université de Liège, Belgium
Florian Frohn – RWTH Aachen University, Germany
Alessandro Gianola – Lisbon University, Portugal
Stéphane Graham-Lengrand – SRI International, US
Alberto Griggio – Fondazione Bruno Kessler, Italy
Martin Jonáš – Masaryk University, Czechia
Alexander Nadel – Technion & Intel, Israel
Aina Niemetz – Stanford University, US
Mathias Preiner – Stanford University, US
Philipp Rümmer – University of Regensburg, Germany
Hans-Jörg Schurr – University of Iowa, US
Natasha Sharygina – University of Lugano, Switzerland
Cesare Tinelli – The University of Iowa, US
Yoni Zohar – Bar-Ilan University, Israel

Contact
All questions about submissions should be emailed to the PC chairs.