5th International Workshop on CPAchecker
September 28th/29th, 2020 online
The goal of the 5th International Workshop on CPAchecker is to bring together researchers and practitioners that are interested in the open-source verification framework CPAchecker. The presentations include new concepts and algorithms in CPAchecker, application to interesting problems, experience reports, and discussion on further directions of the open-source project. The workshop is a presentations-only event, i.e., there are no proceedings.
There will be no registration fee.
However, we will provide the meeting credential only to registered participants. In order to participate in the workshop, you need to register here.
The timezone for the event is Darmstadt local time, i.e. Central European Summer Time, UTC+02:00.
Monday, 28th of September
Speaker: Marie-Christine Jakobs
2:45pm Recent advances of CPAchecker within Klever
Speaker: Evgeny Novikov
This talk will present recent advances of CPAchecker within Klever. I will demonstrate statistics on both the most demanded outcome of software verification tools, that is bugs, and the most frustrating results such as false alarms and unknowns. Even current verification results are magnificent but the future is more promising.
3:30pm Searching for data races with support for RCU
Speaker: Vadim Mutilin
We consider an approach implemented in the CPALockator tool and its key features for supporting programs which use the RCU interface for efficient concurrent synchronization. Namely, we describe RCU analysis with 1) its specific locks and compatibility checks for it and 2) tracking locality of RCU pointers after removal and grace period. The evaluation was performed on benchmarks, based on drivers from the Linux kernel 4.2.6 and known RCU related bugs.
4:00pm Violation Witnesses and Result Validation for Multi-Threaded Programs
Speaker: Karlheinz Friedberger
4:45pm CFA mutations for automatic debugging CPAchecker
Speaker: Pavel Andrianov
5:15pm Fault-Localization with CPAchecker
Speaker: Thomas Lemberger
CPAchecker is one of the most successful tools for finding errors in C programs. After finding an error, CPAchecker does produce a violation witness and a report with the error trace, but its current support for debugging does not go beyond error reporting. This changes with the new fault-localization feature in CPAchecker. With this feature, CPAchecker can use different fault-localization techniques to not only report on errors, but also give hints on potential code faults that caused that error. CPAchecker already supports different fault-localization techniques and provides a generic fault visualization that is integrated in the established report. This talk will present the new fault-localization feature and give a short demo on its usage.
Tuesday, 29th of September
1:30pm Informal Get Together
2:00pm Loop summaries as Horn clauses (ongoing work)
Speaker: Gidon Ernst
2:30pm Cooperative Verification using Invariants
Speaker: Jan Haltermann
Generating strong (loop) invariants is one of the most important tasks in software verification. When a tool lacks finding these, tool developers tend to reimplement other approaches in their tools to overcome that problem. In this talk, I will demonstrate a different strategy: Cooperating with other tools that are already able to generate these invariants to solve the verification task.
3:15pm From Configurable Towards Self-Configuring Program Analysis
Speaker: Cedric Richter
CPAchecker offers a variety of configuration options. It is possible to tune integrated algorithms to a fine level of detail and at the same time to compose complete program analyses to complex verification strategies. Given this flexibility, the integration of a new type of analysis or the extension of existing strategies can easily become a tedious and time-consuming task. In this talk, we present an automatic method to support configuration and report on first experiments with the ultimate goal of a self-configuring CPAchecker.
3:45pm Information Weaving for Test-Case Generation
Speaker: Sebastian Ruland
Information weaving adds new information to the ARG by utilizing the strengthening operator of the LocationCPA. This talk will show current use-cases in test-case generation, which enable us to create more complex test-goals, re-use existing test-suites and speed up the test-case generation process.
4:30pm Panel discussion
Prof. Dr. rer. nat. Marie-Christine Jakobs
Semantics and Verification of Parallel Systems
Office: S2|02 E307
work +49 6151 16-20920