Program

Lightning talks

In addition to full talks, we will have multiple sessions of lightning talks. Each lightning talk is 5 minutes, without discussion. Every participant is encouraged to use this opportunity to quickly present their research and how they use CPAchecker (or would like to use it). Lightning talks can also be used to quickly share ideas and impulses. We can do more than one lightning talk per person, if time permits.

Organization of the lightning talks will be done in the opening of the workshop, so there is no need to register before. There will be enough time for every participant to give at least one lightning talk.

Program

All times are in UTC+2.

Thursday, September 30

Opening (PDF)
Speaker: Thomas Lemberger
Lightning Talks 1
Lightning Talks 2
Coffee Break
Towards Thorough Verification of Particular Critical Industrial C Programs (PDF) (Video)
Speaker: Evgeny Novikov, Anton Vasilyev, Ilja Zakharov
Abstract

During the last decade we have developed the Klever software verification framework intended for verification of large critical industrial C programs like operating system kernels. Thanks to developers of automatic software verification tools (primarily CPAchecker) we could demonstrate good enough results, e.g. here is the list of bugs found by Klever in the Linux kernel and acknowledged by the developers. From the other side it became clear that thorough checking of target programs requires considerable investments in studying program environments and requirements as well as development of corresponding models and specifications. In this talk we will present related challenges and preliminary ideas how one can cope with them. Our next talks will elaborate on the most crucial topics.

Decomposition of Environment Models (PDF) (Video)
Speaker: Ilja Zakharov
Abstract

One of the key problems that can be solved with the Klever software verification framework is thorough verification of a specific software system or its component. Insufficient scalability of employed verification tools may hinder the verification process. The environment model decomposition is a new technique that allows verifying industrial software piecewise in a semi-automatic manner. Its key idea is to develop a single specification for the whole program or program fragment but verify it with different environment models. Such models lead the verification tool to specific places in the program, directly avoiding too many behavioral possibilities in each separate verification task. As a result, the user gets a much better-scaled verification process and a nice list of verdicts for different scenarios of the program behavior verified.

Lunch Break
Virtual Get-Together (coffee break after lunch)
Reusing Predicate Precision in Value Analysis (PDF) (Video)
Speaker: Marie-Christine Jakobs
Abstract

Software verification techniques exchange information to to become more effective and efficient or to increase the trust in the verification result. One information that is to exchanged is precision level of an analysis. So far, precisions are exchanged in the context of regression verification and only between the same analysis. In this talk, we suggest various options to exchange the predicate precision between predicate and value analysis. We discuss our evaluation results for the different exchange options applied to three scenarios, namely, cooperative verification, result validation, and regression verification. Furthermore, we report on comparisons with state-of-the-art techniques for the respective scenarios. To this end, we looked at conditional model checking, witness validation, and the original precision reuse approach.

Internals of Extended Code-Coverage Reports (PDF) (Video)
Speaker: Anton Vasilyev
Abstract

Understanding of CPAchecker analysis timeouts is extremely hard. For this purpose CPAchecker provides statistics and code coverage reports. We propose to enrich code coverage reports by CPA-state information on SMGCPA example.

Coffee Break
An Extensible Invariant Exchange Format for CPAchecker (PDF) (Video)
Speaker: Nico Weise
Representation and Analysis of Code-Coverage Reports from CPAchecker (PDF) (Video)
Speaker: Evgeny Novikov, Vladimir Gratinsky, Ilja Zakharov
Abstract

Code coverage reports are indispensable for users who want to ensure a great quality of verification results. Indeed, some paths in target programs may remain unexplored due to currently incomplete models of their environments. Code coverage reports can help to identify corresponding places very efficiently. Also, they come to the aid when one needs to reveal those parts of target programs that are most complicated for verification tools. This is possible when verification tool developers enrich standard code coverage reports with additional data. CPAchecker does that. In this talk I will present results of the joint work devoted to representation of CPAchecker’s code coverage reports within the Klever software verification framework. In addition, we will go over a couple of real examples.

Friday, October 1

Informal Get-Together
Lightning Talks 3
Software Verification: Historical Landmarks and Current Developments (Video)
Speaker: Dirk Beyer
Coffee Break
Demonstrating the Portfolio Analysis in CPAchecker (PDF) (Video)
Speaker: Thomas Bunk
Abstract

Development teams are integrating formal methods in their software-development workflow. For continuous integration, it is mandatory to have checks with a short response time. State-of-the-art frameworks and setups for comparative evaluation have mostly considered execution of tools on dedicated compute clusters such as StarExec or the VerifierCloud. Those executions are however limited in their parallelism by the number of available processing units. Since recent years, large cloud service providers such as Amazon Web Services (AWS) or Microsoft Azure have emerged on the market, providing users with massively parallel computing infrastructures. In this talk I will present a portfolio algorithm implemented in CPAchecker, an approach in which this verifier aims to exploit the availability of exactly such a setting.

Component-based CEGAR (PDF) (Video)
Speaker: Jan Haltermann
Abstract

CEGAR is a well-known and widely used schema in software verification. Although having this general schema, each tool implements its own CEGAR loop. With our strict decomposition of CEGAR into three loosely coupled components communicating via clearly defined interfaces, we propose a solution to that problem. Providing both a formal definition of the components and interfaces as well as an implementation based on CoVeriTeam and the CPAchecker allows to build a new CEGAR-based tool without reimplementing the whole loop.

Lunch Break
Virtual Get-Together (coffee break after lunch)
Memory Safety Verification with SMGCPA: Results, Challenges and Development Plans (PDF) (Video)
Speaker: Anton Vasilyev
Abstract

Memory safety verification by SMGCPA provides good results on Linux kernel sources with the help of Klever project. Current version of SMGCPA provides a verdict for almost 2/3 of Linux modules, but it seems that the SMG algorithm has a bottleneck in stop/join operations, which prevents analysis of the last 1/3. This talk introduces plans for development of a CEGAR implementation of SMG with a recheck of counterexamples for different assurance in discovery of error.

Program Transformations with CPAchecker (PDF) (Video)
Speaker: Thomas Lemberger
Abstract

Over the years, different program transformations have been integrated in CPAchecker: generation of residual programs, program slicing, program simplifications, program mutations, and more. This talk will not present new research results, but give an overview on some of these transformations and how the existing infrastructure can be leveraged for new research.

Coffee Break
Panel Discussion
Closing

Full talks

Every participant is invited to contribute a talk on their ongoing or latest research and development with and around CPAchecker. Talks will be 20 minutes, +10 minutes time for discussion.

If you want to contribute a talk, please register through the registration form. If you have any questions, contact us.