Monday, September 11
| 9:00 - 9:15 Welcome & Organization | ||
| 9:15 - 10:30 Session 1: Timed and Cyber-Physical Systems | ||
| Dóra Cziborová, Budapest University of Technology and Economics | regular | Combining CEGAR and Lazy Abstraction for Verifying Timed Systems |
| Lena Funk, University of Freiburg | short | Complementation of Phase Event Automata |
| Benedikt Maderbacher, Graz University of Technology | regular | Reactive Synthesis of Cyber-Physical Systems |
| 10:30 - 11:00 Coffee break | ||
| 11:00 - 12:30 Session 2: Markov Decision Processes | ||
| Dániel Szekeres, Budapest University of Technology and Economics | regular | Lazy Abstraction for Markov Decision Processes |
| Maximilian Schäffeler, TU Munich | short | Formally Verified Solution Methods for Factored MDPs |
| Filip Macák, Brno University of Technology | regular | Search and Explore: Symbiotic Policy Synthesis in POMDPs |
| 12:30 - 14:00 Lunch | ||
| 14:00 - 16:00 Session 3: Miscellaneous | ||
| Stefan Ratschan, Czech Academy of Sciences | short | Executing Formal Specifications by Enumeration with Bounds Learning |
| Ondřej Vašíček, Brno University of Technology | regular | Unite: An Adapter for Transforming Analysis Tools to Web Services via OSLC |
| Marek Chalupa, Institute of Science and Technology Austria | regular | Runtime Verification with VAMOS |
| Johannes Haring, Graz University of Technology | short | Automated Verification of Power Contracts |
| Jiri Pavela, Brno University of Technology | regular | A Journey Towards Efficient Profiling |
| 16:00 - 16:30 Coffee break | ||
| 16:30 - 18:00 Session 4: Miscellaneous | ||
| Bernhard Matthias Luedtke, Otto-Friedrich-Universität Bamberg | short | Exploring the Configuration Jungle for Invariant Checking in nuXmv |
| Tobias Nießen, TU Wien | short | Finding counterexamples for ∀∃ hyperproperties |
| Julian Parsert, University of Oxford | regular | Reinforcement Learning for Function Synthesis |
| Stefanie Muroya Lei, Institute of Science and Technology Austria | short | Quantum Information Games for Error-Robust Quantum Algorithms Synthesis |
Tuesday, September 12
| 9:00 - 10:30 Session 5: Decision Procedures and SMT | ||
| Michal Hečko, Brno University of Technology | short | The Tango of Formulae and Automata for Deciding Presburger Arithmetic |
| Tomáš Dacík, Brno University of Technology | short | A Decision Procedure for Strong-Separation Logic |
| Tomáš Kolárik, Institute of Computer Science, Czech Academy of Sciences | regular | Multi-Agent Path Finding with Continuous Time using SMT-LRA |
| Mihály Dobos-Kovács, Budapest University of Technology and Economics | regular | Evaluation of SMT-solvers for abstraction-refinement based model checking |
| 10:30 - 11:00 Coffee break | ||
| 11:00 - 12:30 Session 6: Horn Clauses and SAT | ||
| Martin Blicha, Charles University, Prague & University of Lugano | short | The Golem Horn Solver |
| Konstantin Britikov, Universita della Svizzera Italiana | short | Application of interim Interpolants in the CHC Solving |
| Florian Pollitt, University Freiburg | short | implementing LRAT proofs in CaDiCaL |
| Enrico Lipparini, University of Genoa | short | Satisfiability of Non-Linear Transcendental Arithmetic |
| Jan Kofroň, Charles University | short | YAGA - MCSat-based SMT Solver |
| 12:30 - 14:00 Lunch | ||
| 14:00 - 15:30 Session 7: Provers | ||
| Sarah Tilscher, Technical University of Munich | short | Verifying the Top-Down Solver in Isabelle |
| Philipp Czerner, TU Munich | regular | Making IP = PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms |
| Wolfram Pfeifer, Karlsruhe Institute of Technology | short | Advancements in User Interface of the Deductive Java Verifier KeY |
| Julie Cailler, University of Regensburg | short | Goéland: A Concurrent Tableau-Based Theorem Prover |
| 15:30 - 16:00 Coffee break | ||
| 16:30 - 18:30 Social event | ||
| Guided tour (Clementinum, Old Jewish Quarter, Old Town Square): location of the start is here (in the courtyard, entrance near the address "Karlova 20") | ||
Wednesday, September 13
| 9:00 - 10:30 Session 8: Software Verification | ||
| Thomas Lemberger, LMU Munich | regular | An Experience Report on Automated Software Verification in the Real World |
| Henrik Wachowitz, LMU Munich | regular | Infrastructure for Cooperative Verification |
| Dirk Beyer, LMU Munich | regular | Bridging Hardware and Software Verification using Translations |
| 10:30 - 11:00 Coffee break | ||
| 11:00 - 12:30 Session 9: Complex Systems | ||
| Konstantin Kueffner, Institute of Science and Technology Austria | regular | Statistical Monitoring of Dynamic Systems |
| Mahyar Karimi, Institute of Science and Technology Austria | short | Monitoring Markov Chains |
| Kaushik Mallik, Institute of Science and Technology Austria | short | WIP: Auction-Based Multiobjective Control |
| Levente Bajczi, BME-MIT FTSRG | short | Axiomatic Analysis of Distributed Systems |
| Marcel Ebbinghaus, University of Freiburg | short | Fairness reduction for concurrent programs |
| 12:30 - 14:00 Lunch | ||
| 14:00 - 16:00 Session 10: Hardware Verification | ||
| Vedad Hadžić, Graz University of Technology | regular | Verification of Fault Resistance in Hardware Designs |
| Manuel Bentele, Hahn-Schickard & University of Freiburg | regular | Specification and Verification of Temporal HAL-API Dependencies |
| Nils Froleyks, JKU Linz | short | Certifying Hardware Model Checking |
| Zsófia Ádám, Budapest University of Technology and Economics | short | How Good Are Your Invariants: Witness Validation for Hardware via Circuit Instrumentation with Software Invariants |
| Jan Onderka, Czech Technical University in Prague | regular | Input-based verification and control-flow inference for machine-code systems |
| 16:00 - 16:30 Coffee break | ||
| 16:30 - 17:30 Closing & Discussions | ||