Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Call for Papers: 23rd International Workshop on Satisfiability Modulo Theories

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Call for Papers: 23rd International Workshop on Satisfiability Modulo Theories


Chronological Thread 
  • From: geoff AT cs.miami.edu
  • To: <coq-club AT inria.fr>
  • Subject: [Coq-Club] Call for Papers: 23rd International Workshop on Satisfiability Modulo Theories
  • Date: Tue, 8 Apr 2025 20:22:14 -0400 (EDT)
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=geoff AT cs.miami.edu; spf=SoftFail smtp.mailfrom=geoff AT cs.miami.edu; spf=None smtp.helo=postmaster AT armistead.ccs.miami.edu
  • Ironport-data: A9a23:rw7sZqvF7fh9kME5AwvD4UHdiufnVJhaMUV32f8akzHdYApBsoF/q tZmKWvUbqvfazHye9AiYNzj8UgP75HdyIBrGQs6qy1nFyIXgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRNtspvlDs15K6v4G9A7gRlDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJFskD9EH1sB1O0dHq MRDcyEUd0vcn9vjldpXSsE07igiBMDxOYIEpnxpwXfSBu1gRJHKRqSM6NNFtNsyrpkfR7CFP oxJOHwxBPjDS0Un1lM/B585kumAjWK5djxRrVPTqKYqi4TW5FUoi+i1aoeFJ7RmQ+13k1rBm n/3w1/BLQslG/jH7xrY6jGF07qncSTTBNtISuHmnhJwu3WYwXVWAxkLX3OgsPyhgwi/XcheI goa4EITQbMa/VauT8LhUhS05nWf+BsdUt9RVeA29Wlh15Y4/S6DFFpYURJnauYAvZIOHmc7z 0bSwMvQUGkHXKKudVqR8bKdrDWXMCcTLHMfaSJscefjy4W4yG3Upk6SJuuPAJKIYsvJ9SYcK g1mQQA3nbASltIG3qn99kuBhjOlo5mPQwIojuk2Yo5HxlknDGJGT9b0gbQ+0RqnBNzDJmRtR FBex6CjABkmVPlgVEWlGY3h5o2B6fefKyH7ilVyBZQn/DnF0yf8IdwJu24neRk0bZ1sldrVj Kn74lg5CHh7YCHCUEOLS9/Z5zkCkvS/SI6Nug78N4IeCnSOSON31H03PxDMgQgBYWAxl6AhN I2AcNq9RXEUQaFmxT+3L9rxIpdwrh3TBAr7G/jG8vhQ+ebHOyXKF+9UaQfmgyJQxPrsnTg5O u13b6OioyizmsWnCsUO2d9CcQI5PjIgCIroqsdaUOeGL0A0UCsiEvLdi/dpMYBsg60fxK+C8 2CfS31o7gP1pUTGDgGWNVFlSrfkBqhkoVwBYCcDAFeP2loYW7iJ0psxTZUMUIcCyP1C1t9xF vkMRNWBCK9ASxPB4DUsUqP+p41DKjWuqxOEAC63bBcBf6xLGg74ofr5dDTr9CMxDTeFivFng ry/1zH0RYgIaBRiAf33NtOu7QKVlloMlN1iW3DnJoFoR3zt14xxcQrjo+QSIfATGS7cxzCf6 RmaMS0YqcbJvYUx1tvD3oKAkKuEDMp8GRB8M1TAzLPrKxTfwHWv8bVAXMmMYzrZcmH+o4emR OdNysDDIO81p0lLv6V8AoRU4/oHvfW3nIBjzyNgAHnvRHaoAOk5InC5gO9+hpcUzbpd4QaLS kaD/+dBAoqwOeTnLUUwITQ0ZeHSxNAWnTjvtc4OGnvY3xMu3rS7UhR1BSKu2Qh9N7p+Nb03z dgx4PA27xONsTt0E9KkoB0NyUGyAC0ub6EVuKseIrfXsSsw61QbYZXjGi78u56OTNNXM3gVG DyfhYucprF61G7HKmICKiHV+e9jhpg1mQtryWUaLA+jgev1hf4Q3TxQ/w8oTw9T8A517uJrN kVvNGx3Pa+o/Tx4oORiBUWCQxpgAj+d8WzPk2o5rnXTFRSUZzacPV8DNvao12FH1WBlJxxw3 qySkUThWhbUJPDB5DM4AxNZmqayXO5K11Pwne68FJ64BLg8Wz3uh5GuaUcuqxfKBcAQhlXNl dJ1/dRfOLHKCioNn5IVU4Wq96wcaBShFlxwRftM+KAoH2aFXBqQ3TOICV66e+ITBvjs3HK7N fdTJZN0Z0zj7BqNkzEVPr5TArlWmPVy2sEOVIm2LkE7spyejAFTjrTuygbEilQGee5eyfQGF tuJdhapMHChun9Pqmqc8OhGIjWZZPcHVi3d3ce00ucCBs8fud5CbUgJj7+Gn0iUFCBF/Bukm hzJSIGL7u5lyKVqx5DNFIcaDSqKCNrDbsa62yHtjMZ/Nvb0LtbotSkZjnLFLjZmF+IddPovn IvcreOt+l3OuYgHdlzwmr6DJvFv3tqzVu8GCfDHBiBWsgXaUfC9/iZZ3X6zLKFIt9Zv5sOHY Q+cQ+nofP43X+Zt/lFkWxJ8IT08VZuuNrzBoBmjpcuiEhIeiAzLDO22/E/TMF10SHU6BI3cO CTV5dCV+dFqnKZdDkQlBtZnIaNCDn3NZK8ET+D15B6kVjSGo1XbtrXbwE9qrXmBD3SfC8/17 K7UXhW0Jlz4pKjMy8ofqIBo+AEeCHFmm+QrY0YB4JhMhiunCHIdZ/EoWXnc5kq4TgSpvH05W N3MUIfmISznWDVfbRj17JLoVRzZA+0HP9a/KzA0l69Rh+FaG6vYaIaNNA85i5u1Rtcn5Oq8b 9Qf83jxeBW93/mFgM4Ns+ejj74PKuzynRo1FIOUryA2Kx0FR7AL3XlgWgdBSEQr1i0LeFrjf QAIeIyPfK13pYMd3yqtl7651Sz1ZA/S8gg=
  • Ironport-hdrordr: A9a23:vEYFTqh4h7mYqC4c+YkO3j3IjnBQXrAji2hC6mlwRA09TyX2ra 6TdZggtCMc9gx/ZJhIo7npU5VoKkm3yXca2+Qs1M+ZMDXbhA==
  • Ironport-phdr: A9a23:sWYjphRi6hY71fe4/Ovkj2/ZpdpsonCUAWYlg6HPa5pwe6iut67vI FbYra00ygOSB8ODs7ke07aL6OjJYi8p39WoiDM4TNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL58M hm6txndutUZjYd8Nqo8xRvEr3VVcOlK2G1kIk6ekBn76sqs5pBv9Dhetew8/MBaS6X6eKo4T b1cDDs4Nm0++dPmuxreQwaR/3UQSmoZnAZGDAjD9xH6Q4z+sjDmuepn2SmVJtP5QLYpUjm/9 ahrSRvoiCAaNz4l9Wzcl8J9gL5HrB+nuhdyxZPfboOIO/pkZq7TYM0US21CUMhfVyJMGZ+wY 5cTA+YdJ+tUs5Xxql0TphW+HwmsA+bvxydHhnDo2q063eohHBra0ww7Bd4OtXXUo8/wNKcTS +y60rTHzSjFYvhL1jjz9JLGfQo9ofGQQ71wa8zRxFEgGg7Fklidq4zrMi6a2OgQvWaW8+puW OyshmAntgx8oCajy9kxh4XVmI8YyU3J+yt9zYs0ONC1VEF2bcCrHpZSsSyRKoV4QsQnQ25yu SY6zKULuYO6fCgNxpUo3QTTZOKafIiV5B/oSeWfIS9giX54fL+zmQy+/Ea9xuHmVcS51ExGo ytDn9LRqH0N0wHT6tObSvRj5EevxDeP1gHN5excPEw5m6zWIIM7zLEqjJocq0HDEzf2mEroi K+WcV0p9fKy6+TiY7XmvYOcOJFuhQ7jKKghhtCwAf8iPggLXmiU4+G81Lz58ULnXbpKk+U6k qjfsJ/EOcQWvrO1DgtL3oo55RuzEi2q3dcckHUdLV9JYBeHgJLoO1HKLvD4F/C/g1G0nTdk2 f/GObPhApvWI3ffi7ftZ7N9609Gxwo2zNBT/YxbBawcIP7rXE/+r8TXDgUlPAys3+bnFNJ92 5sDVW6XGK+WLLvSsUOU5uIoO+SDeIgVuC/kJ/c54/7ukGQ2lEQGfaip2JsXcGq3Eu5nI0Wfe 3rsg80OHX0EvgokH6TWjwjWWjlKIn22QqgU5zchCYvgA52VFa63h7nU0yq8EJN+bXsAD1GFF HaueomZCKREUz6bPsI0ym9MbrOmUYJ0jXlG1Sf/wrtjda/P/zEA8InkzJ5z7vHSkhc78Xp1C d6c2ieDVTI8hXsGEhkx2q03uklh0hGby6EtjPFfG9J77OgPVwYzMJ+awuBnWJjpQgyURdCHV HivQ9HuGjQtVpQ0yt4KbVx6HoCtgxfN0QKhGPkQlrWOBdo5/r+Pl2PpKZNbzHDLnLIkk0FgQ sZLMji+gbVj8gHIG4PTu0yDkqexaakV0GjG/3zFyGuHuUAeXQJtOUncdVYYYEae7dHw50eZC qSrFaxiKQxZj8iLNqpNbNTty1RAXvbqftrEMSq3nC+rCBCEy6npDsKicngB3CjbFEkPkhwCt XeAOw8kAy69omXYRDVwHFPrakno/KFwsnS+BkMzygiLaQVm2d/XslYaiPuSRdsYxfQBuS4kq nN5EEv8l9PaBtycphZwKb1GaIB161NG2GTF8g1la8XxdeY53xhOIkIp7CaMn11tB45NkNYnt iYvxQt2cueD1U9ZMiifxdb2M6HWLW/7+FaubbTX0xfQyoXzmO9H5fImplHkpAzsGFAl9iAt3 NRS3XW07Y6MCQsbVJO3X0oqvUsfxfmScmwm6oXY2Gc5e6a5tTHM89kyQu4kwxOhOdpTLenXX B+3GMocCc+0LeUskFX8dRMIMtdZ86ssNt+nff+LsEKyFN1nki6IhGVDqMB420OIrG9nT/LQm o0C27ee1xeGUDH1iBGgtNr2kMZKf2NaEm26wCniYewZLqp8NYkGDmmgC8asgNB/jpvsHXNU6 RaiHBsH3sSteByfYxTh2kVW0lhfrXG8mCS+xiB59lNh5vPOhmqVmqKyJVxZcmdQDHFvl1LtP ZS5g5gBUU6kYhJo3Bqp6EDmxrRK8aF2Lm3dW0BNLE2UZylpVqq9sKbHYtYascJy934OFrTtJ w7JL9y16wEX2C7iAWZEkTUydjXx/478gwQ/k2WFanB6sHvef8h0gxbZ/t3VA/BLjV9kDGF1j yfaAl+kMpyn59KRwt3Mv+ewWUqqTdtWcCDuzMWNuDbxtggISVWv2uu+nNHqC11w3iL82ddCX j6OqRf1Z4it2qine7EvbgxjA1ny7NB/E4d1n94rhZ0e7nMdg42c4XsNlWqgVLcTkbK7dncGQ iQHhsLE+AWwklM2NWqHnsiqHmXY2MZqYMO2J38byj5opd4fE7+atdkm1WN0ugbq9FOLJ6Mk2 GdMj6J0oH8C37NQ4ltrl3rEROtOWxABdS3qnBCV493sm75PaiCgdr+/0Ec4ltekadPK6hdVX HKzEns7NQl36Mg3cFfF0Xmor5rhZMGVdtUL8BudjxbHieFRbpM3jPsDwyR9ayr7ujU+xug3g AYLv9nytZWbK2hr4KOyAwJJfjzzacQJ/zjxjKFY1s+I1oGrF59lF30FRpztBf6vFTsTs7zgO WPsWHUkrWyHHLPEAQKFwE58qnPUD52iOzecL2JfyNRrQRjbKUBCwUgVUDg8gp8lB1WqycjmI yIbrnga4l/1rAcJy/o9bkilFDyG4lf5LGlnLfrXZABb5QxD+UrPZMmX7+YoWjpd4oXktwuVb GqSewVPC2gNHE2CHVHqeLe0tryiu6CVAPSzK/zWbPCAs+tbAr2HyJWh3KNt5HCJN8yKPz9vA +BxiS8hFThpXt/UnTkCUXldjyXWc8uSvwux4AV+tMW+6+jmUQ6p7oCUTb5TONBuvR26nO3QU ozYzDY8IjFe2JQWwHbOw7VKx18ehRZlcDy1GKgBvyrAJEo1sqRMSRsaYiZycsZE8vBktuGiE cXAzNb037t5yPM5FgUePbQAssizYM0RP2y0OBXMD13NMbWPIDyNzs3qM/vUdA==
  • Ironport-sdr: 67f5bdbf_f6MVXmrz+lvSNplyGe1b6xm06VjvU952rKny8QopiBmNIG6 OjHMVjk0UP6Q+oOfyR2DnjvERgOy2em7d1RbhHQ==

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


  • [Coq-Club] Call for Papers: 23rd International Workshop on Satisfiability Modulo Theories, geoff, 04/09/2025

Archive powered by MHonArc 2.6.19+.

Top of Page