Skip to Content.
Sympa Menu

coq-club - [Coq-Club] SMT 2025: Deadline extension

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] SMT 2025: Deadline extension


Chronological Thread 
  • From: geoff AT cs.miami.edu
  • To: <coq-club AT inria.fr>
  • Subject: [Coq-Club] SMT 2025: Deadline extension
  • Date: Tue, 13 May 2025 11:25:06 -0400 (EDT)
  • Authentication-results: mail2-smtp-roc.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:AjlT3a1KMdkQXbOXsfbD5Qd1kn2cJEfYwER7XKvMYLTBsI5bp2cHm jcZCmCDPqmJZzf8L49ybIW+p01V68fUztU2SANu3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn8hlaYDkpOs/je8E4256yo0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW37gkuxMKx8HBo0z5epqWnt05 9lEEwlYO3hvh8ruqF66YuB2g8U4MMTiMMUUsWomyDDQCPdgTJzeK0nIzYYJhnFr34YeTLCAD yYaQWIHgBDobBBINFk/A4l4meahg3i5fjFFwL6QjfBtujiOnFcuitABNvLVRNyQSNkJvH2Zv 2Tg23jWJCwFJZ+QnG/tHnWE2raVw3+lMG4IL5Wz8ecvi1mOzEQIGRgOXB26p+O4gwiwQbpix 1c88zArrLMu+UWnCNLmGRi5qXuF+BMQRrK8DtHW9imIxvvNwSHHN1MEZSFNdYc8jt0TGQcTg wrhc8zSORRjt7icSHS4/7iSrC+vNSV9EYPkTXNeJefiy4W+yLzfni7yosBf/LlZZ+AZ9Bn52 TWLtzQzjrlVhtVN0qSy+FGBjj6xznQocuLXzl6HNo5GxlklDGJAW2BOwQGFhRqnBNzFJmRtR FBex6CjABkmVPlgVEWlGY3h5o2B6fefKyH7ilVyBZQn/DnF0yf8Id8Iv20hdR8ybplsldrVj Kn74lk5CHh7YCLCUEOLS9PZ5zkCkvS/SI6Nug78MooXCnSOSON31H03PxDMgQgBYWAxl6AhN I2AcNq9RXEUQaFmxT+3L9rxIpdxrh3TBAr7G/jG8vhQ+eDFNCbPF+lcawPmgyJQxPrsnTg5O u13b6OioyizmsWnCsUO2d9CcQI5PjIgCIroqsdaUOeGL0A0UCsiEvLdi/dpMYBsg60fxK+C8 2CfS31o7gP1pUTGDgGWNVFlSrfkBqhkoVwBYCcDAFeP2loYW7iJ0psxTZUMUIMcxLRR9sIsF /ghUOecM8tLUQXCqmg8b4GijYlMdyaLpAOpPginayliY5dfaRDAwYLgTCvS9Q0lLCm+he0hq ZKOiyLZRpsiQVx5LcD0MfiA8XK4jUI/qslTAXTaE4J2Q1r91opAJwjarO4FE+tVJTrtnjKlh hurWzEGruzzkqoJ2djuh5Hciby2EuF7T3FoL0OC4ZmYbSDlr3eem6leW+O1fBfYZmP+2IOmQ c53l/jcEvk2rGxmgrpGMYRA7PwBvoP0hrpg0A5bMm3BbA2rBpNeM3C255RzmZMX9IBJmzmde xypwcZbC4WrKcm+MV82JSgZVMqh+8wQuAHv6aUSHB2nyg5xpKGKQGdDDSmq0SZ9FoZ4AKkh4 OUmufMV1TCBtwoXAo6GoBx5p2WoBV4cYpojraAfUdPKiBJ061RsYq78Ky7R4bOPYNAVKkJxG Dulu5Pftu561G7HKmICKiHV+e9jhpg1mQtryWUaLA+jgev1hf4Q3TxQ/w8oTw9T8A517uJrN kVvNGx3Pa+o/Tx4oORiBUWCQxpgAj+d8WzPk2o5rnXTFRSUZzacPV8DNvao12FH1WBlJxxw3 qySkUThWhbUJPDB5DM4AxNZmqayXO5K11Pwne68FJ64BLg8Wz3uh5GuaUcuqxfKBcAQhlXNl dJ1/dRfOLHKCioNn5IVU4Wq96wcaBShFlxwRftM+KAoH2aFXBqQ3TOICV66e+ITBvjs3HK7N fdTJZN0Z0zj7BqNkzEVPr5TArlWmPVy2sEOVIm2LkE7spyejAFTjrTuygbEilUWHupeyfQGF 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:ej7FOa6mE0zGS5o7ywPXwKLXdLJyesId70hD6qkfc3Jom6Cj9v xG4s516facsl94M03I8urrBEDvex7hHOZOjbUsAQ==
  • Ironport-phdr: A9a23:5CSIlhIHY7r3oLRvBtmcuKptWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCEv7M11BSSBdmHt7ptsKn/jePJYS863d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbghGmjaxe69+I Am5oQjfqsUbjoRvJ6kswRbVv3VEfPhbymxvKV+PhRjw4du+8oB++CpKofIh8MBAUaT+f6smS LFTESorPWMo6sD1rBfPVQSA6GcSXWUQiRpIHhPK7ArmUZfrsyv1rfRy1S+HNsDrV780WDCi7 6B2SB/0jSoMKjA0/H3LhsF2kalWpg+qqR5izI7OeIybKeRwcKTec90URWRMRdpdWzBdDo+gd YYDE/YNMOBFpIf9vVsOqh6+CBGjBOzxzT9IiHH20LYm3OQ6Cw3G2Q0gEMgLsHTVttn6KrodU f2zwaLVwjrNc+lY1i3h6IjUbB8hu/eMUKp/fMfR1UQiFQPLg0ifp4D4MT2YyuQDvmaY4uRgS O+iiXArph9srzSz2MohiZTEiIwRx13F6Ch03Ik4KcO3RkN5Z9OvDZVetyafN4RsQ8MiRXllu Ds7yr0Bt5+0ZjIGx4o6yB7CbfGMbouG4gr7WeqMJTp0mmhpdbyiixqo8kWtzvfwW8iy3V1Xs CdFlsTMtmsR1xPN8MiJV/p9/0a/1juXygze5OdJKl0um6XBMZ4u2Lswm4ITsUvdGi/2n137g 7WMdkUh++io8Pjnbav8qZCBLYN7lh3xMr80lsy6AOQ3KA0OX2mB9euiybLj4FX1QLRMjvIoj qnUqI3WKMAFqqKjDQJZz5wv5hW7Aju80dkUhXwHI0hEeBKDgYjpIVbOIPXgAPewnVuslzlrx /7dM7L9GZXBNH3DkLb7crZ46k5Q0hQ8ws1C555MDLEOO+r8WlXtu9zAEh85Lwu0zv76BNllz IMRRXqPArOFMKPVqVKH+uUvI/CVaIAJvDb9NuMq6uX1jX45nF8dZbOm0YEWaHC+BPRmIl+Wb WDigtcbQi82uV9qR+vzzVaGTDR7ZnCoXqt66CttW6y8CoKWSY2qjrKp1zz9G5xfY2EAB1yRQ iSgTJmNR/pZMHHaGcRmiDFRDdBJKqck3BCq7krhzqZ/a/DT8WsevI7i095846vSkwsz/Hp6F ZfVyHmDGkdzmG5AXDoqxOZnu0UoxVqE36ZQiOceEN1a4vIPXwsnZtbH1+IvMNf8RizIf9PBU 1O6WpOjCDA1QMg2xooBbkFzFf2plVbG3iOvAvkYm6HYTIcs/Pf62H78b914126A1KQliAw+R dBTMGS9mqNl3wHJAo/Sj0iQm+Chfr9a2S/E8WbFwGaT1K1BeCh3V6iNHXUWZ0+M6M/8+luHV bilT7IuLgpGz8eGbKpMcNzgy1tcFr/lP5zFbmS9ln3VZ17Az66QbIfsZ2QW3TnMQEkCnQcJ+ H+aNA84Ti6/qmPaBTZqGBrheUTpueV5rXq6SAczwWToJwVu2r279DYenrqZSvoW3/QJtDpg4 zR4EVCh3s7HXsKarlkpd6FdbNUhpVZfgDuI7UomZ9rwfuY81Tt8O0xtskjj1gt6ENBFmMku9 jYxyRZqbLif2xVHfi+Z2pb5PvvWLHPz9Vahcf2zuBmW3dCI96MI8Pl9pU/kuVTjGUcl/XtP2 MIT1nqV45SMAQYPG8GUMA5/511hqrfWbzNorYzZ0nNiGaKv9DrD0tcoQuYp11zzN8caO6SCG gjoFsQcDMX7M+0mlW+iaRccNfxT/qo5Vy+/X8CB1rKFNedk1HKjhGVDusVm116UsjB7QajO1 ooExPeR2k2GUS39hRGvqJK/lYdBbDAUewj3gS/qTIFcYaN8VY0QT2KvKsi2gNhymtbsQDZZ8 lWnBlUL1Ie1flKUaEC10QBL1EsRqGCq/Enwh2UlyXdy9+zPjWqQi+35PAIKIGtKWHVvgR/3L I64gspbFEmkYg41lQe0sEPzxqxVvqN6fAyxCQ9Deyn7KX0nU7Pl7+vYJZUWrsN593sENYb0K UqXQbP8vRYAhibqHm8EgSs+aynvoJLy2RpzlGOaKn936nvfY8B5gxnFt7m+DbZc2CQLQC5gh HzZHF+5apOm8NKamb/Iqaa7VmukV9tefTShnubi/GOroHZnBxGyhaX5ldDgHwYS2jS90thjU CSOoRrhKNqjx+GxNuRpeVNtDVn35p9hG41wpYA3gYkZxXkQgpjGmBhP2Xe2K9hQ3rjyKWYcX TNeicCA+xDrgQcwZmLM3Y/yUW+Rh9dsd8XvKH1DwToztqUoQO+V9OAWxHov5AHh61KAJ6En1 jYFlal3si9c2r5Q/lFxiHzESrEUFk1FMSG+oA+Q4Zaxq6JYYGvper+1sSg21caoCLXIyu1Fc FD+fJpqXSp578EldUnJzGW28IbvPt/ZcdMUsBSQ1RbGlelcbpwrxLIMgmJ8NGTxsGdAqaZzh AFy3Zy8oImMKnl8tKO/DBlCMzTpZsQVsjjzhKdal8yS0sihBJJkUjkMWZLpS7qvHldw/bz/M B2SFTQntnqBMbPFGA6E9EpvozTEGIvtMnCeIXhfwNl/BVGcKEFZnAEITWA6k5o+RWXIjITqd EZ04CxU50at80oWjLkxcUmuFDmMwWXgIi05Q5WeMhdMuwRL5kOPdNeb8vo2BSZTuJuosA2KL GWfIQVOF2AAHEKeVDWBdvGj48fN9++AC6+wNfzLNP+BpOtQWd+D3tSq04Jj/nCBOtjFbRwAR 7Urn1FOW3x0AZGTgzIUVykejD7AdeaSvhK94TF6p8z5+//wHgfu7I6OTbZeLJ88nnL+ybfGP OmWiiFjLD9e3Z5Z3n7Exo8U21sKgj1vfT2geVzlnSXWCqfRk6pWSRMXdnErXCOnx6knmAxMM MvazN75y+wj5hbUI15fUF36hsygaYoBKHr7MVLOAUfNObibd2Wj/g==
  • Ironport-sdr: 6823645c_ZjM9kCBU/l6M5Zh9z9BP67joq/1EzZYlsmBTdU+h1yBwg5i IxbIyw8leBiLjz/paVri4ab2oAC2lrw+cHhdFXQ==

Due to multiple requests, we have decided to extend the deadlines for
submissions to the SMT workshop. For helping with the organization, we added
an abstract deadline. Here are the new dates:

Abstract deadline (new): May 16th, 2025
Submission deadline (extended): May 22nd, 2025

Jochen and Sophie,
SMT 2025 workshop chairs

The full call is here:
=======================================================================
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/
Abstract deadline (new): May 16th, 2025
Submission deadline (extended): May 22nd, 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] SMT 2025: Deadline extension, geoff, 05/13/2025

Archive powered by MHonArc 2.6.19+.

Top of Page