5th International Workshop on CPAchecker (CPA'20)

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.

5th International Workshop on CPAchecker

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.

Date and Location

September 28th/29th, 2020 online

Registration

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.

Program

The timezone for the event is Darmstadt local time, i.e. Central European Summer Time, UTC+02:00.

Monday, 28th of September

2:00pm Opening

Speaker: Marie-Christine Jakobs

2:45pm Recent advances of CPAchecker within Klever

Speaker: Evgeny Novikov

Slides (opens in new tab)

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:15pm Break

3:30pm Searching for data races with support for RCU

Speaker: Vadim Mutilin

Slides (opens in new tab)

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

Slides (opens in new tab)

TBA

4:30pm Break

4:45pm CFA mutations for automatic debugging CPAchecker

Speaker: Oleg Petrov

Slides

When a CPAchecker bug occurs, it is useful for debugging to have a small input program to reproduce the same bug. We have implemented an algorithm that reduces an input program without changing the analysis result. Our algorithm is based on the Delta Debugging approach. According to it, analysis is run multiple times. Each time the CFA is simplified a bit (mutated). If the result of the analysis differs from the initial one, the CFA change is reverted. The process ends when there are no possible mutations. The result CFA may be translated into C code.

The talk describes an algorithm, implementation details, and results on several programs with an introduced bug. The line number of the programs was reduced by four times, and the operator number was reduced by two orders of magnitude.

5:15pm Fault-Localization with CPAchecker

Speaker: Thomas Lemberger

Slides (opens in new tab)

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

Slides (opens in new tab)

TBA

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:00pm Break

3:15pm From Configurable Towards Self-Configuring Program Analysis

Speaker: Cedric Richter

Slides (opens in new tab)

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

Slides (opens in new tab)

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:15pm Break

4:30pm Panel discussion

5:30pm Closing

Organization

Picture: Benjamin Raddatz

Prof. Dr. rer. nat. Marie-Christine Jakobs

Semantics and Verification of Parallel Systems

Contact