SMT 2024: 22ND INTERNATIONAL WORKSHOP ON SATISFIABILITY MODULO THEORIES
PROGRAM

Days: Monday, July 22nd Tuesday, July 23rd

Monday, July 22nd

View this program: with abstractssession overviewtalk overview

08:30-09:00Breakfast/Coffee
09:00-10:30 Session 1: Verification and Theories
Chair:
Mathias Preiner
09:00
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Marco Roveri and Stefano Tonetta
Verification Modulo Theories - presentation-only submission (abstract)
PRESENTER: Alessandro Cimatti
09:30
Hichem Rami Ait El Hara, François Bobot and Guillaume Bury
An SMT Theory for n-Indexed Sequences [Extended abstract] (abstract)
PRESENTER: Guillaume Bury
10:00
Thomas Hader and Alex Ozdemir
An SMT-LIB Theory of Finite Fields [Original Paper] (abstract)
10:30-11:00Coffee Break
11:00-12:00 Session 2: Invited Talk
Chair:
Giles Reger
11:00
Sophie Tourret
The Hows and Whys of Higher-Order SMT (abstract)
12:00-14:00Lunch Break (Not Provided)
14:00-15:30 Session 3: Applications
Chair:
Katalin Fazekas
14:00
Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonáš and Greg Kimberly
Efficient SMT-based Analysis of Failure Propagation - presentation only submission (abstract)
PRESENTER: Alessandro Cimatti
14:30
Arijit Shaw and Kuldeep S. Meel
CSB: A Counting and Sampling tool for Bit-vectors [Extended Abstract] (abstract)
PRESENTER: Arijit Shaw
15:00
Guillaume Bury
Minimal logic detection and exporting smtlib problems with Dolmen [Extended abstract] (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 4: SMT-COMP
16:00
Martin Bromberger
SMT-COMP Results and Tool Presentations
Tuesday, July 23rd

View this program: with abstractssession overviewtalk overview

08:30-09:00Breakfast/Coffee
09:00-10:30 Session 5: Proofs and Strategies
Chair:
Clark Barrett
09:00
Alessio Coltellacci, Stephan Merz and Gilles Dowek
Reconstruction of SMT proofs with Lambdapi [original paper] (abstract)
PRESENTER: Alessio Coltellacci
09:30
Katalin Fazekas, Florian Pollitt, Mathias Fleury and Armin Biere
Certifying Incremental SAT Solving [Presentation only] (abstract)
PRESENTER: Katalin Fazekas
10:00
Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel Day, Florin Manea and Vijay Ganesh
Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis [Presentation only] (abstract)
PRESENTER: Zhengyang Lu
10:30-11:00Coffee Break
11:00-12:00 Session 6: Invited Talk
Chair:
Yoni Zohar
11:00
Mathias Preiner
Challenges in Bit-Vector Reasoning (abstract)
12:00-14:00Lunch Break (Not Provided)
14:00-15:30 Session 7: Decision Procedures
Chair:
Sophie Tourret
14:00
Max Barth and Matthias Heizmann
A Bit-vector to Integer Translation with bv2nat and nat2bv [Extended abstract] (abstract)
PRESENTER: Max Barth
14:30
Ahmed Irfan and Stephane Graham-Lengrand
Arrays Reasoning in MCSat [Original Paper] (abstract)
PRESENTER: Ahmed Irfan
15:00
Guilherme Toledo, Yoni Zohar and Clark Barrett
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness [Presentation only] (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 8: SMT-LIB and Business Meeting
Chair:
Aina Niemetz
16:00
Clark Barrett
SMT-LIB Report
16:45
Giles Reger
SMT Business Meeting