SMT PROGRAM
Days: Thursday, August 11th Friday, August 12th
Thursday, August 11th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 120H: Invited talk #1
Chair:
Location: Ullmann 311
| 09:00 | Local Search for Bit-Precise Reasoning and Beyond (abstract) |
| 10:00 | Trail saving in SMT (abstract) PRESENTER: Milan Banković |
10:30-11:00Coffee Break
11:00-12:30 Session 125M: Arithmetics and higher-order reasoning
Chair:
Location: Ullmann 311
| 11:00 | Bit-Precise Reasoning via Int-Blasting (abstract) PRESENTER: Yoni Zohar |
| 11:20 | An SMT Approach for Solving Polynomials over Finite Fields (abstract) PRESENTER: Thomas Hader |
| 11:40 | On Satisfiability of Polynomial Equations over Large Prime Fields (abstract) PRESENTER: Lucas Vella |
| 12:00 | Goose: A Meta Solver for Deep Neural Network Verification (abstract) PRESENTER: Joseph Scott |
12:30-14:00Lunch Break
Lunches will be held in Taub hall and in The Grand Water Research Institute.
14:00-15:30 Session 127M: Tools
Location: Ullmann 311
| 14:00 | NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems (abstract) PRESENTER: Anna Becchi |
| 14:20 | cvc5: A Versatile and Industrial-Strength SMT Solver (abstract) PRESENTER: Andres Noetzli |
| 14:40 | The VMT-LIB Language and Tools (abstract) PRESENTER: Alessandro Cimatti |
| 15:00 | Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (abstract) PRESENTER: Mathias Preiner |
15:30-16:00Coffee Break
16:00-17:30 Session 131K: SMT-COMP Report and Tool Presentation
Chair:
Location: Ullmann 311
| 16:00 | SMT-COMP Report and Tool Presentations |
18:00-19:30Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event
Friday, August 12th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 134D: Celebrating 20 years of the SMT workshop
Chair:
Location: Taub 2
| 09:00 | Panel discussion "SMT: Past, Present and Future" PRESENTER: Cesare Tinelli |
| 10:00 | CDSAT for nondisjoint theories with shared predicates: arrays with abstract length (abstract)  PRESENTER: Maria Paola Bonacina |
10:30-11:00Coffee Break
11:00-12:30 Session 137E: Theories and Proofs
Chair:
Location: Taub 2
| 11:00 | User-Propagators for Custom Theories in SMT Solving (abstract) PRESENTER: Clemens Eisenhofer |
| 11:20 | An SMT-LIB Theory of Heaps (abstract) PRESENTER: Zafer Esen |
| 11:40 | Challenges and Solutions for Higher-Order SMT Proofs (abstract) PRESENTER: Mikolas Janota |
| 12:00 | A simple proof format for SMT (abstract) PRESENTER: Jochen Hoenicke |
12:30-14:00Lunch Break
Lunches will be held in Taub hall.
14:00-15:30 Session 138E: Standards and benchmarks - Business meeting
Chair:
Location: Taub 2
| 14:00 | SMT-Lib Update Report PRESENTER: Cesare Tinelli |
| 14:30 | Business Meeting PRESENTER: Antti Hyvärinen |
15:30-16:00Coffee Break
16:00-16:45 Session 139C: Update on Proof Standardization (Joint Session with PAAR) (joint with PAAR)
Chair:
Location: Taub 7
| 16:00 | SMT Proof Standardization Update |