Click on the title of a talk to read the abstract.

The program will be also available as PDF here once it is finalized.

Tuesday, Oct. 1st, 2019

10:00–12:00 Session 1

1.0 Welcome
Dirk Beyer
(LMU Munich, Germany)
1.1 Ultimate Automizer
Matthias Heizmann
(University of Freiburg)
1.2 LTL Software Model Checking in CPAchecker
Thomas Bunk
(LMU Munich)
slides
1.3 CPALockator: Thread-Modular Approach with Transition Abstraction for Analysis of Multithreaded Software
Pavel Andrianov
(ISPRAS)
slides

12:00–13:00 Lunch

13:00–14:00 Session 2

2.1 Cooperative Verification
Dirk Beyer
(LMU Munich, Germany)
slides
2.2 Differential Modular Software Verification
Marie-Christine Jakobs
(TU Darmstadt)

14:30–18:00 Social Event

18:00 Workshop Dinner

Our workshop dinner will take place at the Klosterwirt

Wednesday, Oct. 2nd, 2019

9:00–10:30 Session 4:

4.1 Interpretation-based Witness Validation for C code
Philipp Berger
(RWTH Aachen)
slides
4.2 VerifyThis tasks in sv-benchmarks
Gidon Ernst
(LMU Munich)
slides
4.3 Current Development of CPAchecker
Philipp Wendler
(LMU Munich)
slides

11:00–12:00 Session 5

5.1 Symbiotic with CPAchecker
Marek Chalupa
(Masaryk University, Brno)
slides
5.2 Hunting for Bugs and Works in Linux Driver Verification project
Vadim Mutilin
(ISPRAS)
slides

12:00–13:00 Lunch

13:00–15:00 Session 6

2.3 Regression Test-Case Generation with CPAchecker
Sebastian Ruland
(TU Darmstadt)
slides
2.4 Reducing time and efforts when verifying large software systems with Klever
Ilja Zakharov
(ISPRAS)
slides
3.1 Symbolic Memory Graphs in CPAchecker
Karlheinz Friedberger
(LMU Munich)
slides
3.2 Symbolic Memory Graphs invariants and corresponding optimizations for SMGCPA
Anton Vasilyev
(ISPRAS)
slides

15:00–15:30 Coffee break

15:30–17:00 Session 3

3.3 Static verification results visualization in the context of SV-COMP
Vitaly Mordan
(ISPRAS)
slides
6.1 Panel Discussion
Alexej Khoroshilov
(ISPRAS)

18:00 Workshop Dinner

Our workshop dinner will take place at the Klosterwirt