PROGRAM
Days: Sunday, August 10th Monday, August 11th
Sunday, August 10th
View this program: with abstractssession overviewtalk overview
09:15-09:30 Session 1: Welcome
Location: JMS 641
09:30-10:30 Session 2: Invited Talk
Chair:
Location: JMS 641
| 09:30 | Deciding Satisfiability of Quantified Bitvector Formulae with BDDs (abstract)  |
10:30-11:00Coffee Break
11:00-12:20 Session 3: Quantifier Instantiation and Combination of Theories
Chair:
Location: JMS 641
| 11:00 | Quantifier Instantiations: To Mimic or To Revolt? (abstract) |
| 11:20 | From MBQI to Enumerative Instantiation and Back (abstract) PRESENTER: Marek Dančo |
| 11:40 | Being Polite is Not Enough (and Other Limits of Theory Combination) (abstract) PRESENTER: Guilherme Toledo |
| 12:00 | A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints (abstract) PRESENTER: Pascal Fontaine |
12:20-13:30Lunch Break
13:30-15:00 Session 4: Theories
Chair:
Location: JMS 641
| 13:30 | Evaluating Binary Polynomials using Subpolynomials (abstract) PRESENTER: Jacob M. Howe |
| 14:00 | Satisfiability Modulo Exponential Integer Arithmetic (abstract) PRESENTER: Florian Frohn |
| 14:20 | Constraint Propagation for Bit-Vectors in Alt-Ergo (abstract) PRESENTER: Basile Clément |
| 14:40 | Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search (abstract) PRESENTER: Stéphane Graham-Lengrand |
15:00-15:30Coffee Break
15:30-17:10 Session 5: Applications
Chair:
Location: JMS 641
| 15:30 | Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2 (abstract) |
| 15:50 | Space Explanations of Neural Network Classification (abstract) PRESENTER: Tomáš Kolárik |
| 16:10 | Approximate SMT Counting Beyond Discrete Domains (abstract) |
| 16:30 | Syntax-Guided Synthesis with Counterexample-Guided E-graphs: A Work-in-Progress Report (abstract) PRESENTER: Guy Frankel |
| 16:50 | On Writing SMT-LIB Scripts: Metrics and a New Dataset (abstract) PRESENTER: Soaibuzzaman |
Monday, August 11th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 6: Invited talk + Optimization Modulo Theory
Chair:
Location: BO LT1
| 09:00 | SAT Reasoning in CDCL(T) Solvers (abstract) |
| 10:00 | An Optimization Modulo Theories-Based Approach to Cumulative Scheduling with Delays (abstract) PRESENTER: Antton Kasslin |
10:30-11:00Coffee Break
11:00-12:30 Session 7: Solvers + Benchmarks + SMT-LIB
Chair:
Location: BO LT1
| 11:00 | Visualization of Execution Traces in Colibri 2 SMT Solver (abstract) |
| 11:20 | A Conjecture Regarding SMT Instability (abstract) |
| 11:40 | A Catalog of SMT-LIB Benchmarks (abstract) |
| 12:00 | A Proposal for an OMT Extension to SMT-LIB (abstract) PRESENTER: Nestan Tsiskaridze |
12:30-13:30Lunch Break
13:30-15:00 Session 8: SMT-COMP
Chair:
Location: BO LT1
| 13:30 | Instability Track for SMT-COMP (abstract) PRESENTER: Marijn Heule |
| 13:50 | SMT-COMP Presentation PRESENTER: François Bobot |
15:00-15:30Coffee Break
15:30-17:00 Session 9: SMT-LIB Discussion + Business Meeting
Chairs:
Location: BO LT1
| 15:30 | SMT-LIB Discussion |
| 16:15 | Business Meeting PRESENTER: Sophie Tourret |
