The scientific program starts at 14:00 on Monday and it is planned to be finished at 14:00 on Thursday.

Each regular (student) presentation will have a 20 minute time budget, we suggest you to give a 15 minutes long presentation and have 5 minutes for the questions.

Bus travel is organized from Budapest to Visegrád: departure at 11:00 AM, Monday, from Keleti Railway station (Keleti pályaudvar). More details will come later.

Bus travel is organized on Thursday back to Budapest, arriving at Budapest, Keleti railway station at 16:00.


Tutorial: Gabriel Ebner LEAN
Invited: Alfons Laarman LTSmin: Exploiting Locality for High-Performance, Language-Independent Model Checking
Session 1: Valentin Touzeau Full cache analysis combining abstract interpretation and model checking approach
Sepideh Asadi HiFrog: SMT-based Function Summarization for Software Verification
Matthias Dangl A Unifying View on SMT-based Software Verification
Session 2: Dániel Darvas Finding bugs in the LHC: Verification methods for PLC programs
Dogan Ulus On the quantitative semantics of regular expression over real-valued signals
Ayrat Khalimov Bounded Synthesis for Branching Logics
Invited: Ufuk Topcu Adaptable Yet Provably Correct Autonomous Systems
Session 3: Petr Novotny Probabilistic programming
Pranav Ashok Value Iteration for Long-run Average Reward in Markov Decision Processes
Philipp J. Meyer Synthesis of controllers for CPS
Benjamin Bichsel Symbolic Reasoning for Probabilistic Programs
Invited: Xiaowei Huang Verification of Robotics and Autonomous Systems
Invited: Dino Distefano INFER
Session 4: Henning Günther Automated Verification of Parallel Software with IC3
Ivan Radicek Automated Clustering and Program Repair for Introductory Programming Assignments
Andreas Humenberger Algebraic Reasoning about Programs
Matteo Marescotti Distributed Model Checking using SMT
Invited: Bernhard K. Aichernig Smart Black-box Testing – Combining Model Learning and Model-based Testing
Session 5: Thomas Lemberger Tests from Witnesses: Execution-Based Validation of Verification Results
Adrian Rebola Pardo Interpolation for DRAT Proofs
Andreas Fellner Branching Search for Model Based Mutation Testing
Session 6: Alireza Abyaneh Self-Referential Theorem Proving in Selfie
Benjamin Kiesl Proofs in SAT Solving
 Martin Blicha  Focused Interpolants
Katalin Fazekas Combining SMT with QBF and MaxSAT
Session 7: Mirco Giacobbe Model checking hybrid systems
Laura Nenzi System design of stochastic models using robustness of temporal properties.
Sebastian Arming SEA PARAM: Exploring Schedulers in Parametric MDPs
Florian Lonsing Evaluating QBF Solvers: Quantifier Alternations Matter