Accepted Papers

Original Papers

  • Automated Reasoning with Nested Datatypes
    Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, Cesare Tinelli
  • Exploration Heuristics for the NuCAD and CAlC Algorithms
    Alexej Kolbin, Jasper Nalbach, Erika Ábrahám
  • Floating‑Point Arithmetic of Symbolic Size in SMT‑LIB 3
    Kristoffer Norrman, Tjark Weber
  • A Modern View on MCSat
    Thomas Hader, Theo Jauschneg, Daniela Kaufmann, Laura Kovacs
  • An Eager Encoding of Array Summation Constraints
    Patrick Janoschek, Roland Herrmann, Philipp Rümmer
  • Accelerating Parallel SMT Solving with Fixed First Decisions
    Amalee Wilson, Andrew Reynolds, Robert Jones, Cesare Tinelli, Clark Barrett

Extended Abstracts

  • Local Reasoning with Expressive Array Specifications
    Rodrigo Raya, Christophe Ringeissen
  • SMT-based Automation for Overwhelming Truth: A Polymorphic and Higher-Order Extension
    David Baelde, Stéphanie Delaune, Stanislas Riou
  • Extending the cvc5 Relational Solver with Cyclicity Reasoning
    Rachel Cleaveland, Mudathir Mohamed, Clark Barrett, Caroline Trippel, Cesare Tinelli

Presentation-Only Papers

  • Characterizing Sets of Theories That Can Be Disjointly Combined
    Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar
  • Efficient Volume Computation for SMT Formulas
    Arijit Shaw, Uddalok Sarkar, Kuldeep S. Meel
  • Learning Unified Graph and Language Representations for SMT Algorithm Selection
    Zhengyang (John) Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea, Vijay Ganesh
  • MCSAT Modulo Transcendental Arithmetics
    Jorge Gallego Hernández, Enrico Lipparini, Alessio Mansutti
  • LLM2SMT: Building an SMT Solver with Zero Human-Written Code
    Mikoláš Janota, Mirek Olšák
  • Incremental Linearization for Quantified Nonlinear Integer Arithmetic
    Marek Dančo, Mikoláš Janota, Karel Chvalovsky