Thursday, August 11th, 2022

9:00-10:30 Session 1

Chair: David Deharbe
Room: Ullman 311

  • Local Search for Bit-Precise Reasoning and Beyond (Invited talk). Aina Niemetz (60 min).
  • Trail saving in SMT. Milan Banković and David Šćepanović.
10:30-11:00 Coffee break
11:00-12:30 Session 2: arithmetics and higher-order reasoning

Chair: Sophie Tourret
Room: Ullman 311

  • Bit-Precise Reasoning via Int-Blasting. Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Noetzli, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli.
  • An SMT Approach for Solving Polynomials over Finite Fields. Thomas Hader and Laura Kovacs.
  • On Satisfiability of Polynomial Equations over Large Prime Fields. Lucas Vella and Leonardo Alt.
  • Goose: A Meta Solver for Deep Neural Network Verification. Joseph Scott, Guanting Pan, Elias Khalil and Vijay Ganesh.
12:30-14:00 Lunch
14:00-15:30 Session 3: tooling

Chair: Bruno Dutertre
Room: Ullman 311

  • NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems. Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella and Marco Zamboni.
  • cvc5: A Versatile and Industrial-Strength SMT Solver. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mahgoub Yahia Mohamed, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar.
  • The VMT-LIB Language and Tools. Alessandro Cimatti, Alberto Griggio and Stefano Tonetta.
  • Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. Aina Niemetz, Mathias Preiner and Clark Barrett.
15:30-16:00 Coffee break
16:00-17:30 Session 4

Chair: Aina Niemetz
Room: Ullman 311

  • SMT-COMP report & tool presentations. Haniel Barbosa, Francois Bobot and Jochen Hoenicke.

Friday, August 12th, 2022

9:00-10:30 Session 5

Chair: Antti Hyvärinen
Room: Taub 2

  • Panel discussion "SMT: Past, Present and Future" (60 min). Clark Barrett, Maria-Paola Bonacina, Bruno Dutertre, Roberto Sebastiani, Cesare Tinelli (moderator)
  • CDSAT for nondisjoint theories with shared predicates: arrays with abstract length. Maria Paola Bonacina, Stéphane Graham-Lengrand and Natarajan Shankar.
10:30-11:00 Coffee break
11:00-12:30 Session 6: theories and proofs

Chair: Yoni Zohar
Room: Taub 2

  • User-Propagators for Custom Theories in SMT Solving. Nikolaj Bjørner, Clemens Eisenhofer and Laura Kovacs.
  • An SMT-LIB Theory of Heaps. Zafer Esen and Philipp Ruemmer.
  • Challenges and Solutions for Higher-Order SMT Proofs. Chad Brown, Mikolas Janota and Cezary Kaliszyk.
  • A simple proof format for SMT. Jochen Hoenicke and Tanja Schindler.
12:30-14:00 Lunch
14:00-15:30 Session 7

Chair: Antti Hyvärinen
Room: Taub 2

  • SMT-LIB benchmark update & SMT-LIB language update (30 min). Clark Barrett, Cesare Tinelli and Pascal Fontaine.
  • Business meeting (60 min).
15:30-16:00 Coffee break
16:00-16:45 Session 8: Update on Proof Standardization (joint session with PAAR)

Chair: Cesare Tinelli
Room: Taub 7

  • SMT Proof Standardization Update. Haniel Barbosa.
  • Discussions.