Each student talk will have 20 minutes (15 minutes for the presentation + 5 minutes for the questions)!

The timing is the following, for the session details please visit the program page.

Alpine Verification Meeting 2017 Program
Monday Tuesday Wednesday Thursday
9:00 Ufuk Topcu Session
6 (4 talks)
9:30 Dino Distefano
10:30 Travel
to Visegrád
Coffee break Coffee break / posters Coffee break
11:00 Session
3 (4 talks)
4 (4 talks)
7 (4 talks)
12:00 Registration
/ Lunch
12:30 Lunch Lunch Lunch
14:00 Gabriel Ebner Xiaowei Huang Bernhard K. Aichernig Travel
to Budapest
15:00 Alfons Laarman
15:30 Coffee break Posters
+ Coffee
Coffee break
16:00 Session
1 (3 talks)
5 (3 talks)
16:30 Roundtable
/ Discussion
17:00 Break Trip
17:30 Session
2 (3 talks)
18:30 Dinner
19:00 Dinner Dinner
20:30 Game night / Spa


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