The program is still in preparation. The workshop will take place August 10-11, 2025.

List of Accepted Papers

  • Florian Frohn and Jürgen Giesl. Satisfiability Modulo Exponential Integer Arithmetic (presentation only)
  • Guilherme Toledo, Benjamin Przybocki and Yoni Zohar. Being polite is not enough (and other limits of theory combination) (presentation only)
  • Tomáš Kolárik, Faezeh Labbaf, Martin Blicha, Michael Wand, Natasha Sharygina and Grigory Fedyukovich. Space Explanations of Neural Network Classification (presentation only)
  • Jacob M. Howe, Martin Brain and Arnau Gàmez-Montolio. Evaluating Binary Polynomials using Subpolynomials (original paper)
  • Jan Jakubuv and Mikoláš Janota. Quantifier Instantiations: To Mimic or To Revolt? (extended abstract)
  • Arijit Shaw and Kuldeep S. Meel. Approximate SMT Counting Beyond Discrete Domains (presentation only)
  • Marek Dančo, Petra Hozzová and Mikoláš Janota. From MBQI to Enumerative Instantiation and Back (extended abstract)
  • Guy Frankel, Rudi Schneider, Michel Steuwer and Elizabeth Polgreen. Syntax-Guided Synthesis with CounterExample Guided E-graphs: A Work-In-Progress Report (extended abstract)
  • Christophe Junke and François Bobot. Vizualization of execution traces in Colibri 2 SMT solver (extended abstract)
  • Soaibuzzaman and Jan Oliver Ringert. On Writing SMT-LIB Scripts: Metrics and a new Dataset (extended abstract)
  • Antton Kasslin and Jeremias Berg. An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays (original paper)
  • Marcel Barlik and Martin Brain. Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2 (extended abstract)
  • Amar Shah, Yi Zhou, Marijn Heule and Bryan Parno. Instability Track for SMT-COMP (extended abstract)
  • Hichem Rami Ait-El-Hara, Guillaume Bury, Basile Clément and Pierre Villemot. Constraint Propagation for Bit-Vectors in Alt-Ergo (extended abstract)
  • Can Cebeci, Nikolaj Bjørner, George Candea and Clément Pit-Claudel. A Conjecture Regarding SMT Instability (extended abstract)
  • Ellen Dasnois and Pascal Fontaine. A Few Exercices on the Complexity of Congruence Closure with Cardinality Constraints (extended abstract)
  • Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli and Clark Barrett. A Proposal for an OMT Extension to SMT-LIB (orignal paper)
  • Hans-Jörg Schurr, Mathias Preiner, Aina Niemetz, Clark Barrett, Pascal Fontaine and Cesare Tinelli. A Catalog of SMT-LIB Benchmarks (presentation only)
  • Enrico Lipparini, Thomas Hader, Ahmed Irfan and Stéphane Graham-Lengrand. Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search (presentation only)