The program mainly consists of talks given by the participants on their recent results or ongoing research. Social events include a joint dinner and an excursion.
During registration, you can indicate whether you want to give a talk. The duration of the talk is either 10min or 25min. Please also specify a preliminary title and a short preliminary abstract for your talk. After each talk, there will be 5min time for questions from the audience. Between talk sessions, we will have coffee breaks. Lunch is also provided.
Keynote
The meeting will open with a keynote by Philipp Rümmer, University of Regensburg and Uppsala University, on Automatic Program Instrumentation for Automatic Verification.
Social Program
The social program begins with a joint dinner on Wednesday evening. On Thursday afternoon, we will have an excursion to the Schauinsland mountain and Germany’s longest circulating cable car, the Schauinslandbahn. In the evenings, after the end of the official programs, there will be social gatherings, where we can chat and play games.
Full Program
Tuesday, September 3
| 19:00 – 23:00 | Pre-Conference Socializing (Feierling Biergarten) |
Wednesday, September 4
| 08:45 – 09:00 |  Opening |
Andreas Podelski |
| 09:00 – 10:00 | Keynote session chair: Andreas Podelski |
|
| 09:00 |  Automatic Program Instrumentation for Automatic Verification (slides) |
Philipp Rümmer, University of Regensburg and Uppsala University |
| 10:00 – 10:30 | Invariants session chair: Andreas Podelski |
|
| 10:00 | Invariant slicing by accessibility (slides) | Ilgiz Mustafin, Constructor Institute |
| 10:15 | Collections of class invariants (slides) | Alessandro Schena, Constructor Institute |
| 10:30 – 11:00 | Coffee Break | |
| 11:00 – 12:30 | SAT & Quantified Boolean Formulas session chair: Mathias Fleury |
|
| 11:00 | Deciding Boolean Separation Logic via Small Models (slides) | Tomáš Dacík, Brno University of Technology, Faculty of Information Technology |
| 11:30 | NapSAT and Debugging Infrastructure Engineering | Robin Coutelier, TU Wien |
| 11:45 | Hierarchical Stochastic SAT and Quality Assessment of Logic Locking (slides) | Tobias Seufert, University of Freiburg |
| 12:00 | Skolem Functions for false QBFs (slides) | Peter Pfeiffer, Johannes Kepler University |
| 12:15 | PyQBF - A Python Framework for Solving Quantified Boolean Formulas (slides) | Mark Peyrer, Johannes Kepler University |
| 12:30 – 14:00 | Lunch | |
| 14:00 – 15:35 | Common Formalisms & Exchange Formats session chair: Frank Schüssele |
|
| 14:00 | Towards a formally verified operational-semantics framework (slides) | Jan Tusil, Masaryk University |
| 14:30 | Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification (slides) | Gidon Ernst, LMU Munich |
| 14:45 | Software Verification Witnesses (slides) | Marian Lingsch-Rosenfeld, LMU Munich |
| 15:00 | Software Engineering Meets Program Verification: Incremental Development & Continuous Checking (slides) | Manuel Bentele, Hahn-Schickard |
| 15:15 | Towards Scalable and Distributed Software Verification (slides) | Dirk Beyer, LMU Munich |
| 15:30 | VASSAL – Verification and Analysis for Safety and Security of Applications in Life (slides) |
Filip Macák, Brno University of Technology |
| 15:35 – 16:00 | Coffee Break | |
| 16:00 – 17:30 | Automata & Graphs session chair: Matthias Heizmann |
|
| 16:00 | A new approach on the termination of parameterized transition systems (slides) | Roland Herrmann, University of Regensburg |
| 16:30 | Parametrized Automata over Infinite Alphabets (slides) | Franziska Alber, University of Regensburg |
| 16:45 | Efficient Graph-Based Reachability Analysis (slides) | Attila Ficsor, Budapest University of Technology and Economics |
| 17:15 | Repetitive Substructures for Efficient Representation of Automata (slides) | Michal Šedý, Faculty of Information Technology, Brno University of Technology |
| 19:00 – 20:00 | Dinner | |
| 20:00 – 23:00 | Game Night |
Thursday, September 5
| 09:00 – 10:30 | Software & Hardware session chair: Manuel Bentele |
|
| 09:00 | A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification (slides) | Po-Chun Chien, LMU Munich |
| 09:30 | Bridging verification of levels of digital systems using machine-check (slides) | Jan Onderka, Czech Technical University in Prague |
| 10:00 | Verifying Multipliers with Symbolic Computer Algebra by Order and Phase Optimization (slides) | Alexander Konrad, University of Freiburg |
| 10:30 – 11:00 | Coffee Break | |
| 11:00 – 12:30 | Synthesis & Analysis of Systems session chair: Dominik Klumpp |
|
| 11:00 | Guiding Synthesis with AI (slides) | Julian Parsert, University of Innsbruck |
| 11:15 | Reactive Synthesis modulo Theories (slides) | Benedikt Maderbacher, TU Graz |
| 11:45 | Verifying Unsolvability in Classical Planning with VeriPB (slides) | Simon Dold, University of Basel |
| 12:00 | Monitors, Systems, and Privacy (slides) | Mahyar Karimi, IST Austria |
| 12:15 | Scalable Redundancy Detection for Real-Time Requirements (slides) | Lena Funk, University of Freiburg |
| 12:30 – 13:45 | Lunch | |
| 14:00 – 18:30 | Excursion |
Friday, September 6
| 09:00 – 10:30 | SMT & Constrained Horn Clauses session chair: Tanja Schindler |
|
| 09:00 | Automata-Based Decision Procedures Meet Solving String Constraints (slides) | David Chocholatý, Brno University of Technology, Faculty of Information Technology |
| 09:30 | String Solving in Z3 (slides) | Clemens Eisenhofer, TU Wien |
| 09:45 | An Update on the OpenSMT Solver (slides) | Tomas Kolarik, University of Lugano |
| 10:00 | Efficient Manipulation of Logical Formulas as Decision Diagrams (slides) | Milán Mondok, Budapest University of Technology and Economics |
| 10:15 | CHC Solving in Stainless (slides) | Sankalp Gambhir, EPFL |
| 10:30 – 11:00 | Coffee Break | |
| 11:00 – 12:30 | Quantitative Analyses & Neural Networks session chair: Matthias Heizmann |
|
| 11:00 | Policies Grow on Trees: Model Checking Families of MDPs (slides) | Filip Macák, Brno University of Technology |
| 11:30 | Safety and Liveness of Quantitative Properties and Automata | N. Ege Saraç, ISTA |
| 11:45 | Abstraction-based timed model checking for software-intensive system models (slides) | Dóra Cziborová, Budapest University of Technology and Economics |
| 12:15 | Formal Reasoning on Neural Networks (slides) | Faezeh Labbaf, University of Lugano |
| 12:30 – 14:00 | Lunch | |
| 14:00 – 15:45 | Software Model Checking session chair: Andreas Podelski |
|
| 14:00 | End-to-End Validation of Input Model Transformations in Model Checking Tools (slides) | Zsófia Ádám, Budapest University of Technology and Economics |
| 14:30 | Reachability analysis of multiloop software using TPA (slides) | Konstantin Britikov, University of Lugano (USI) |
| 14:45 | Detection and integration of conditional commutativity for concurrent program verification (slides) | Marcel Ebbinghaus, University of Freiburg |
| 15:15 | Challenges for memory-model-aware verification (slides) | Levente Bajczi, Budapest University of Technology and Economics |
| 15:45 – 15:50 | Closing Remarks |
Andreas Podelski |
| 15:50 – 15:55 | AVM’25 |
Roderick Bloem |
| 15:55 – 16:30 | Post-Conference Coffee Break |