SMT — PROGRAM
Days: Friday, 24 July 2026 Saturday, 25 July 2026
Friday, 24 July 2026
08:45-09:00
Welcome
SMT
Location:
C1.04
09:00-10:30
Invited Talk + Encodings
SMT
Location:
C1.04
| 09:00-10:00 |
SAT-Guided Gröbner Basis Methods for Arithmetic Circuit Verification (abstract) 60 min
1 TU Wien
|
| 10:00-10:30 |
An Eager Encoding of Array Summation Constraints (abstract) 30 min
1 University of Regensburg
2 Uppsala University, University of Regensburg
|
10:00-11:00
Coffee Break
SMT
Location:
C1.04
11:00-12:30
MCSat & Nonlinear Arithmetic
SMT
Location:
C1.04
| 11:00-11:30 |
A Modern View on MCSat (abstract) 30 min
1 TU Wien
|
| 11:30-12:00 |
MCSAT Modulo Transcendental Arithmetics (abstract) 30 min
1 IMDEA Software
2 University of Cagliari
|
| 12:00-12:30 |
Exploration Heuristics for the NuCAD and CAlC Algorithms (abstract) 30 min
1 RWTH Aachen University
|
12:30-14:00
Lunch
SMT
Location:
C1.04
14:00-15:30
Decision Procedures & Automation
SMT
Location:
C1.04
| 14:00-14:30 |
Incremental Linearization for Quantified Nonlinear Integer Arithmetic (abstract) 30 min
1 Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC)
|
| 14:30-15:00 |
SMT-based Automation for Overwhelming Truth: A Polymorphic and Higher-Order Extension (abstract) 30 min
1 Univ Rennes, CNRS, IRISA
|
| 15:00-15:30 |
Floating‑Point Arithmetic of Symbolic Size in SMT‑LIB 3 (abstract) 30 min
1 Uppsala University
|
15:30-16:00
Coffee Break
SMT
Location:
C1.04
16:00-17:30
Learning, LLMs & Counting
SMT
Location:
C1.04
| 16:00-16:30 |
LLM2SMT: Building an SMT Solver with Zero Human-Written Code (abstract) 30 min
1 Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC)
|
| 16:30-17:00 |
Learning Unified Graph and Language Representations for SMT Algorithm Selection (abstract) 30 min
1 University of Waterloo
2 University of Göttingen and CIDAS
3 Georgia Institute of Technology
|
| 17:00-17:30 |
Efficient Volume Computation for SMT Formulas (abstract) 30 min
1 Chennai Mathematical Institute
2 Indian Statistical Institute
3 Georgia Institute of Technology
|
Saturday, 25 July 2026
09:00-10:30
Invited Talk + Parallelism
SMT
Location:
C1.04
| 09:00-10:00 |
From Distributed SAT to Distributed SMT? Successes and Challenges (abstract) 60 min
1 Karlsruhe Institute of Technology
|
| 10:00-10:30 |
Accelerating Parallel SMT Solving with Fixed First Decisions (abstract) 30 min
1 Stanford University
2 The University of Iowa
3 AWS
|
10:30-11:00
Coffee Break
SMT
Location:
C1.04
11:00-12:30
Arrays, Datatypes & Relational Reasoning
SMT
Location:
C1.04
| 11:00-11:30 |
Automated Reasoning with Nested Datatypes (abstract) 30 min
1 Bar-Ilan University
2 University of Iowa, Amazon
3 Stanford University
4 The University of Iowa
|
| 11:30-12:00 |
Local Reasoning with Expressive Array Specifications (abstract) 30 min
1 Technical University of Madrid, Spain
2 Université de Lorraine, CNRS, Inria, LORIA, 54000 Nancy, France
|
| 12:00-12:30 |
Extending the cvc5 Relational Solver with Cyclicity Reasoning (abstract) 30 min
1 Stanford University
2 The University of Iowa
|
12:30-14:00
Lunch
SMT
Location:
C1.04
14:00-15:30
SMT
SMT
Location:
C1.04
| 14:00-14:30 |
Characterizing Sets of Theories That Can Be Disjointly Combined (abstract) 30 min
1 Carnegie Mellon University
2 Bar-Ilan University
|
| 14:30-15:30 |
SMT-LIB Discussion (abstract) 60 min
1 The University of Iowa
|
15:30-16:00
Coffee Break
SMT
Location:
C1.04
16:00-17:30
SMT-COMP & Business Meeting
SMT
Location:
C1.04
| 16:00-17:00 |
SMT-COMP Presentation (abstract) 60 min
1 University of Manchester
|
| 17:00-17:30 |
Business Meeting (abstract) 30 min
1 Universidade Federal de Minas Gerais
|