PROGRAM
Friday, July 24th
08:45-09:00 Session 1: Welcome
09:00-10:30 Session 2: Invited Talk + Datatypes
09:00
Daniela Kaufmann (TU Wien)
Invited talk: SAT-Guided Gröbner Basis Methods for Arithmetic Circuit Verification
10:00
Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett and Cesare Tinelli
Automated Reasoning with Nested Datatypes
10:30-11:00Coffee Break
11:00-12:30 Session 3: MCSat & Nonlinear Arithmetic
11:00
Thomas Hader, Theo Jauschneg, Daniela Kaufmann and Laura Kovacs
A Modern View on MCSat
11:30
Jorge Gallego Hernández, Enrico Lipparini and Alessio Mansutti
MCSAT Modulo Transcendental Arithmetics
12:00
Alexej Kolbin, Jasper Nalbach and Erika Ábrahám
Exploration Heuristics for the NuCAD and CAlC Algorithms
12:30-14:00Lunch Break
14:00-15:30 Session 4: Decision Procedures & Automation
14:00
Marek Dančo, Mikoláš Janota and Karel Chvalovsky
Incremental Linearization for Quantified Nonlinear Integer Arithmetic
14:30
David Baelde, Stéphanie Delaune and Stanislas Riou
SMT-based Automation for Overwhelming Truth: A Polymorphic and Higher-Order Extension
15:00
Kristoffer Norrman and Tjark Weber
Floating-Point Arithmetic of Symbolic Size in SMT-LIB 3
15:30-16:00Coffee Break
16:00-17:30 Session 5: Learning, LLMs & Counting
16:00
Mikoláš Janota and Mirek Olšák
LLM2SMT: Building an SMT Solver with Zero Human-Written Code
16:30
Zhengyang (John) Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea and Vijay Ganesh
Learning Unified Graph and Language Representations for SMT Algorithm Selection
17:00
Arijit Shaw, Uddalok Sarkar and Kuldeep S. Meel
Efficient Volume Computation for SMT Formulas
Saturday, July 25th
09:00-10:30 Session 6: Invited Talk + Parallelism
09:00
Dominik Schreiber (Karlsruhe Institute of Technology)
Invited talk: From Distributed SAT to Distributed SMT? Successes and Challenges
10:00
Amalee Wilson, Andrew Reynolds, Robert Jones, Cesare Tinelli and Clark Barrett
Accelerating Parallel SMT Solving with Fixed First Decisions
10:30-11:00Coffee Break
11:00-12:30 Session 7: Arrays, Datatypes & Relational Reasoning
11:00
Patrick Janoschek, Roland Herrmann and Philipp Rümmer
An Eager Encoding of Array Summation Constraints
11:30
Rodrigo Raya and Christophe Ringeissen
Local Reasoning with Expressive Array Specifications
12:00
Rachel Cleaveland, Mudathir Mohamed, Clark Barrett, Caroline Trippel and Cesare Tinelli
Extending the cvc5 Relational Solver with Cyclicity Reasoning
12:30-14:00Lunch Break
14:00-15:30 Session 8: SMT
14:00
Benjamin Przybocki, Guilherme V. Toledo and Yoni Zohar
Characterizing Sets of Theories That Can Be Disjointly Combined
14:30
Pascal Fontaine, Cesare Tinelli
SMT-LIB Discussion
15:30-16:00Coffee Break
16:00-17:30 Session 9: SMT-COMP & Business Meeting
16:00
Martin Jonas
SMT-COMP Presentation
17:00
Haniel Barbosa
Business Meeting