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

The program is also available as PDF.

Thursday, Sept. 22, 2016

9:00–10:30 Session 1: Perspectives

Welcome / History of CPAchecker
Dirk Beyer
(LMU Munich, Germany)
CPAchecker and Linux Driver Verification
Alexey Khoroshilov
(ISP RAS, Russia)
Bringing Formal Verification Closer to Practicing Engineers: The mbeddr Approach
Daniel Ratiu
(Siemens, Germany)

11:00–12:00 Session 2: Infrastructure

CPAchecker: Towards Large-Scale Bug Discovery
George Karpenkov
(VERIMAG, France)
Benchmarking with Containers
Philipp Wendler
(University of Passau, Germany)

13:30–15:00 Session 3: Improvements and Experiments

Modeling Memory with Memory Regions for Predicate Abstractions
Vadim Mutilin
(ISP RAS, Russia)
Several Recent Experiments with Predicate Analysis
Mikhail Mandrykin
(ISP RAS, Russia)
Further Development of Methods for Verifying Several Properties at Once
Vitaly Mordan
(ISP RAS, Russia)

15:30–17:00 Session 4: Reuse of Verification Results and Concurrency

Our Reuse of the Abstract Reachability Graph
Marie-Christine Jakobs
(University of Paderborn, Germany)
Extension of CPA Approach for Efficient Analysis of Parallel Programs
Pavel Andrianov
(ISP RAS, Russia)
A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker
Karlheinz Friedberger
(University of Passau, Germany)

18:00 Workshop Dinner

Our workshop dinner will take place in the Greek restaurant ''Akropolis Athen'' (Rudolf-Guby-Str. 1), which is located very close to the university campus.

Friday, Sept. 23, 2016

9:00–10:30 Session 5: Configurable Program Analyses

SMT-Based Software Model Checking
Matthias Dangl
(University of Passau, Germany)
Effective Approaches to Abstraction Refinement for an Explicit-Value Analysis
Stefan Löwe
(University of Passau, Germany)
Using Configurable Program Analysis on Machine Code
Sven Mattsen
(Hamburg University of Technology, Germany)

11:00–12:00 Session 6: Memory Safety

Lazy Heap Analysis with Symbolic Memory Graphs
Alexander Driemeyer
(University of Passau, Germany)
Checking Memory Safety with SMGCPA
Anton Vasilyev
(ISP RAS, Russia)

13:30–15:30 Session 7: Algorithms and Theories

Augmenting Predicate Analysis with Auxiliary Invariants
Thomas Stieglmaier
(University of Passau, Germany)
Towards Unbounded Heap Support for Predicate Analysis using SMT Arrays
Stephan Lukasczyk
(University of Passau, Germany)
Implementing Termination Analysis using Configurable Software Verification
Sebastian Ott
(University of Passau, Germany)
Implementing PDR in CPAchecker
Gernot Zorneck
(University of Passau, Germany)

16:00–17:00 Session 8: Open Problems

Software Verification: Real Challenges
Evgeny Novikov
(ISP RAS, Russia)
Directing CPAchecker State Exploration with the Help of Hints from a Linux Driver Environment Model for More Efficient Bug Finding
Ilia Zakharov
(ISP RAS, Russia)

17:00–17:30 Session 9: Closing, Discussion, and Outlook