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:00 | ||||
| 10:30 | Travel to Visegrád |
Coffee break | Coffee break / posters | Coffee break |
| 11:00 | Session 3 (4 talks) |
Session 4 (4 talks) |
Session 7 (4 talks) |
|
| 11:30 | ||||
| 12:00 | Registration / Lunch |
|||
| 12:30 | Lunch | Lunch | Lunch | |
| 13:00 | ||||
| 13:30 | ||||
| 14:00 | Gabriel Ebner | Xiaowei Huang | Bernhard K. Aichernig | Travel to Budapest |
| 14:30 | ||||
| 15:00 | Alfons Laarman | |||
| 15:30 | Coffee break | Posters + Coffee |
Coffee break | |
| 16:00 | Session 1 (3 talks) |
Session 5 (3 talks) |
||
| 16:30 | Roundtable / Discussion |
|||
| 17:00 | Break | Trip | ||
| 17:30 | Session 2 (3 talks) |
|||
| 18:00 | ||||
| 18:30 | Dinner (banquet) |
|||
| 19:00 | Dinner | Dinner | ||
| 19:30 | ||||
| 20:00 | ||||
| 20:30 | Game night / Spa | |||
| 21:00 | ||||
Program:
| 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 |