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.
|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|
|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|