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 EconomicsregularCombining CEGAR and Lazy Abstraction for Verifying Timed Systems
Lena Funk, University of FreiburgshortComplementation of Phase Event Automata
Benedikt Maderbacher, Graz University of TechnologyregularReactive 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 EconomicsregularLazy Abstraction for Markov Decision Processes
Maximilian Schäffeler, TU MunichshortFormally Verified Solution Methods for Factored MDPs
Filip Macák, Brno University of TechnologyregularSearch and Explore: Symbiotic Policy Synthesis in POMDPs
12:30 - 14:00  Lunch
14:00 - 16:00  Session 3: Miscellaneous
Stefan Ratschan, Czech Academy of SciencesshortExecuting Formal Specifications by Enumeration with Bounds Learning
Ondřej Vašíček, Brno University of TechnologyregularUnite: An Adapter for Transforming Analysis Tools to Web Services via OSLC
Marek Chalupa, Institute of Science and Technology AustriaregularRuntime Verification with VAMOS
Johannes Haring, Graz University of TechnologyshortAutomated Verification of Power Contracts
Jiri Pavela, Brno University of TechnologyregularA Journey Towards Efficient Profiling
16:00 - 16:30  Coffee break
16:30 - 18:00  Session 4: Miscellaneous
Bernhard Matthias Luedtke, Otto-Friedrich-Universität BambergshortExploring the Configuration Jungle for Invariant Checking in nuXmv
Tobias Nießen, TU WienshortFinding counterexamples for ∀∃ hyperproperties
Julian Parsert, University of OxfordregularReinforcement Learning for Function Synthesis
Stefanie Muroya Lei, Institute of Science and Technology AustriashortQuantum 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 TechnologyshortThe Tango of Formulae and Automata for Deciding Presburger Arithmetic
Tomáš Dacík, Brno University of TechnologyshortA Decision Procedure for Strong-Separation Logic
Tomáš Kolárik, Institute of Computer Science, Czech Academy of SciencesregularMulti-Agent Path Finding with Continuous Time using SMT-LRA
Mihály Dobos-Kovács, Budapest University of Technology and EconomicsregularEvaluation 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 LuganoshortThe Golem Horn Solver
Konstantin Britikov, Universita della Svizzera ItalianashortApplication of interim Interpolants in the CHC Solving
Florian Pollitt, University Freiburgshortimplementing LRAT proofs in CaDiCaL
Enrico Lipparini, University of GenoashortSatisfiability of Non-Linear Transcendental Arithmetic
Jan Kofroň, Charles UniversityshortYAGA - MCSat-based SMT Solver
12:30 - 14:00  Lunch
14:00 - 15:30  Session 7: Provers
Sarah Tilscher, Technical University of MunichshortVerifying the Top-Down Solver in Isabelle
Philipp Czerner, TU MunichregularMaking IP = PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms
Wolfram Pfeifer, Karlsruhe Institute of TechnologyshortAdvancements in User Interface of the Deductive Java Verifier KeY
Julie Cailler, University of RegensburgshortGoé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 MunichregularAn Experience Report on Automated Software Verification in the Real World
Henrik Wachowitz, LMU MunichregularInfrastructure for Cooperative Verification
Dirk Beyer, LMU MunichregularBridging 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 AustriaregularStatistical Monitoring of Dynamic Systems
Mahyar Karimi, Institute of Science and Technology AustriashortMonitoring Markov Chains
Kaushik Mallik, Institute of Science and Technology AustriashortWIP: Auction-Based Multiobjective Control
Levente Bajczi, BME-MIT FTSRGshortAxiomatic Analysis of Distributed Systems
Marcel Ebbinghaus, University of FreiburgshortFairness reduction for concurrent programs
12:30 - 14:00  Lunch
14:00 - 16:00  Session 10: Hardware Verification
Vedad Hadžić, Graz University of TechnologyregularVerification of Fault Resistance in Hardware Designs
Manuel Bentele, Hahn-Schickard & University of FreiburgregularSpecification and Verification of Temporal HAL-API Dependencies
Nils Froleyks, JKU LinzshortCertifying Hardware Model Checking
Zsófia Ádám, Budapest University of Technology and EconomicsshortHow Good Are Your Invariants: Witness Validation for Hardware via Circuit Instrumentation with Software Invariants
Jan Onderka, Czech Technical University in PragueregularInput-based verification and control-flow inference for machine-code systems
16:00 - 16:30  Coffee break
16:30 - 17:30  Closing & Discussions