PROGRAM
Days: Wednesday, September 24th Thursday, September 25th Friday, September 26th
Wednesday, September 24th
View this program: with abstractssession overviewtalk overview
09:00-09:50 Session 1: Invited talk: Daniela Kaufmann
Chair:
Location: A102
| 09:00 | Verifying Arithmetic Circuits with Polynomials (abstract) |
10:20-11:30 Session 3: AVM Opening Remarks and First Presentations - Certificates and Witnesses
Chair:
Location: A210
| 10:20 | LIV: Loop-Invariant Validation Using Straight-Line Programs (abstract) |
| 10:50 | From Interleavings to Owicki–Gries via Empires: Certificates for Concurrent Program Verification (abstract) |
12:00-13:00 Session 4: Tutorial - Nikolaj Bjørner
Chair:
Location: A210
| 12:00 | Arithmetic Solving in Z3 (abstract) |
14:00-15:00 Session 5: Tutorial - Andrei Voronkov
Chair:
Location: A210
| 14:00 | First-Order Proof Checking (abstract) |
15:30-17:30 Session 7: Presentations - Networks and Optimizations
Chair:
Location: A210
| 15:30 | Proof-based Space Explanation of Classifying Neural Networks (abstract) |
| 16:00 | On the Verification of Structured Parameterized Networks (abstract) PRESENTER: Neven Villani |
| 16:30 | Hardware-Optimal Quantum Algorithms (abstract) PRESENTER: Stefanie Muroya |
| 17:00 | Positive Almost-Sure Termination of Polynomial Random Walks (abstract) |
18:00-22:00 Trip to Recas Winery and SYNASC/AVM Conference Dinner
Dinner with wine tasting at Winery Recas (organized trip by bus, busses leave at 6pm from the AVM venue).
Thursday, September 25th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 8: Presentations - Verification and Synthesis
Chair:
Location: A210
| 09:00 | Formal Verification with Configurable Execution Semantics (abstract) |
| 09:30 | Computing abstract model-checking transitions using abstract interpretation (abstract) |
| 10:00 | Parameterized Infinite-State Reactive Synthesis (abstract) |
10:30-10:40 Session 9: Group Photo
Location: A210
11:00-11:50 Session 11: Invited Talk: Thomas A. Henzinger
Chair:
Location: A102
| 11:00 | Neural Certificates (abstract) |
12:10-13:10 Session 12: Ask-us-Anything
Q&A and discussion with Daniela Kaufmann, Thomas A. Henzinger, and Natasha Sharygina
Location: A210
14:00-16:00 Session 13: Presentations - Automata
Chair:
Location: A210
| 14:00 | Regexes with Back-References using Register Set Automata (abstract) |
| 14:30 | Towards Minimizing Phase Event Automata (abstract) |
| 15:00 | Complementing Emerson-Lei Elevator Automata (abstract) |
| 15:30 | Learning Mealy Machines with Sparse Observation Tables (abstract) PRESENTER: Wolffhardt Schwabe |
16:30-18:30 Session 15: Presentations - Symbolic Execution and Static Analysis
Chair:
Location: A210
| 16:30 | Accelerating Decision-diagram-based Quantum Circuit Simulation With Symbolic Execution (abstract) |
| 17:00 | RacerF: Lightweight Static Data Race Detection for C Code (abstract) |
| 17:30 | Witness-guided verification in trace abstraction (abstract) |
19:00-22:00 AVM Dinner
AVM Dinner and Networking at Beraria 700
Friday, September 26th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 17: Presentations - SMT and Applications
Chair:
Location: A210
| 09:00 | Current State of String Solver Z3-Noodler (abstract) |
| 09:30 | On User-defined Decision Guidance in SMT Solvers (abstract) |
| 10:00 | Pseudo-Boolean Proof Logging for Optimal Classical Planning (abstract) PRESENTER: Simon Dold |
11:00-12:00 Session 19: Presentations - SAT and Proofs
Chair:
Location: A210
| 11:00 | Proofs (that contain programs that contain proofs)* (abstract) |
| 11:30 | Robust by Design: SAT-based Automata Learning in the Presence of Noise (abstract) |
