3rd International Workshop on CPAchecker and 8th Linux Driver Verification Workshop

The joint 3rd International Workshop on CPAchecker (CPA) and 8th Linux Driver Verification (LDV) Workshop
will take place on September 25-26, 2018 in Moscow, Russia.

About

The goal of the workshop is to bring together researchers and practitioners that work in the area of functional, safety, and security verification of real-life software written in C and that are interested in the open-source verification framework CPAchecker. The presentations at the workshop include specifics of real-world verification of C programs, experience reports, new concepts and algorithms in CPAchecker, and discussion on further directions.

Organizers

The workshop is organized by the Ivannikov Institute for System Programming Russian Academy of Sciences.
For questions please feel free to contact Vadim Mutilin, email: mutilin@ispras.ru, tel: +7 (495) 912-53-17 ext. 4454.

Venue

Workshop Location
109004, Moscow, Alexander Solzhenitsyn st., 25.
Directions.

Traveling to Moscow
You can directly fly to Moscow from practically all the largest international airports. You may also make unforgettable trip to Moscow by train.

Visa Information
If you need an invitation letter to apply for a visa, such can be provided to attendees. Please send your request by e-mail to mutilin@ispras.ru and provide scan copy of your passport.

Registration

If you plan or think of participating in the workshop, we request you to fill out this form.

Please fill out the form as soon as possible and do not hesitate to register, when you are not sure about your participation (the form will have an option for this).

Filling out the form helps us to better plan and organize the workshop.

Program
Tuesday, September 25th
09:00 - 11:00
Dirk Beyer - Reducer-Based Construction of Conditional Verifiers

Despite recent advances, software verification remains challenging. To solve hard verification tasks, we need to leverage not just one but several different verifiers employing different technologies. To this end, we need to exchange information between verifiers. Conditional model checking was proposed as a solution to exactly this problem: The idea is to let the first verifier output a condition which describes the state space that it successfully verified and to instruct the second verifier to verify the yet unverified state space using this condition. However, most verifiers do not understand conditions as input. In this paper, we propose the usage of an off-the-shelf construction of a conditional verifier from a given traditional verifier and a reducer. The reducer takes as input the program to be verified and the condition, and outputs a residual program whose paths cover the unverified state space described by the condition. As a proof of concept, we designed and implemented one particular reducer and composed three conditional model checkers from the three best verifiers at SV-COMP 2017. We defined a set of claims and experimentally evaluated their validity. All experimental data and results are available for replication.

Matthias Dangl - Algorithm Selection

Software verification is the concept of determining, given an input program and a specification, whether the input program satisfies the specification or not. There are different strategies that can be used to approach the problem of software verification, but, according to comparative evaluations, none of the known strategies is superior over the others. Therefore, many tools for software verification leave the choice of which strategy to use up to the user, which is problematic because the user might not be an expert on strategy selection. In the past, several learning-based approaches were proposed in order to perform the strategy selection automatically. This automatic choice can be formalized by a strategy selector, which is a function that takes as input a model of the given program, and assigns a verification strategy. Our goal is to identify a small set of program features that (1) can be statically determined for each input program in an efficient way and (2) sufficiently distinguishes the input programs such that a strategy selector for picking a particular verification strategy can be defined that outperforms every constant strategy selector.
Our results can be used as a baseline for future comparisons, because our strategy selector is simple and easy to understand, while still powerful enough to outperform the individual strategies. We evaluate our feature set and strategy selector on a large set of 5687 verification tasks and provide a replication package for comparative evaluation.

Pavel Andrianov - Thread Modular Configurable Program Analysis
Karlheinz Friedberger - Domain-Independent Multi-threaded Software Model Checking

Recent development of software aims at massively parallel execution, because of the trend to increase the number of processing units per CPU socket. But many approaches for program analysis are not designed to benefit from a multi-threaded execution and lack support to utilize multi-core computers. Rewriting existing algorithms is difficult and error-prone, and the design of new parallel algorithms also has limitations. An orthogonal problem is the granularity: computing each successor state in parallel seems too fine-grained, so the open question is to find the right structural level for parallel execution. We propose an elegant solution to these problems: Block summaries should be computed in parallel. Many successful approaches to software verification are based on summaries of control-flow blocks, large blocks, or function bodies. Block-abstraction memoization is a successful domain-independent approach for summary-based program analysis. We redesigned the verification approach of block-abstraction memoization starting from its original recursive definition, such that it can run in a parallel manner for utilizing the available computation resources without losing its advantages of being independent from a certain abstract domain. We present an implementation of our new approach for multi-core shared-memory machines. The experimental evaluation shows that our summary-based approach has no significant overhead compared to the existing sequential approach and that it has a significant speedup when using multi-threading.

11:00 - 11:30 Coffee break
11:30 - 13:00
Marie-Christine Jakobs - Cooperative Test Case Generation

For more than 20 years, verifiers have been used for test generation. However, verifiers have different strength and weaknesses. Generating a test-case covering a particular program branch will be easy for one verifier while it might be difficult for another verifier. Inspired by abstraction-driven concolic testing and recent advances in cooperative software verification, we combine different verifiers for test-case generation. Our hope is that such a combination increases the number of test goals (e.g. program branches) covered by the generated test-cases.
In this talk, we present how we integrated test-case generation with multiple verifiers into CPAchecker and explain the available options, e.g., which information to exchange between verifiers. Furthermore, we report on our experience using combinations of predicate and value analysis for test-case generation.

Sebastian Ruland - Test Generation with CPAchecker
Philipp Wendler - New Developments in BenchExec

This talk will present two new features of BenchExec. The first feature is the measurement of energy consumption of runs. Developing energy-efficient algorithms is becoming more important, and a first necessary step is to be able to measure energy consumption. We will also see that this can provide new insights about the efficiency of existing tools.
The second feature, which is still in development, is a new metadata format for verification tasks. This format will allow to specify additional information about tasks to make BenchExec usable in more scenarios, such as for verification tasks with several input files.

13:00 - 14:00 Launch
14:30 - 19:00 Walk with excursion around the city
19:00 Restaurant
Wednesday, September 26th
09:00 - 11:00
Thomas Lemberger - Incremental Slicing

We present a new, iterative static program slicing technique that uses counterexample-guided abstraction refinement to iteratively compute slicing criteria and build incremental slices. For slicing, we use static program slicing based on a dependence graph directly tied to the CFA of CPAchecker, using data-flow and control dependences.

Mikhail Mandrykin - Slicing and Scope Bounded Verification with Polymorphic Region and Effect Inference

The talk presents a kind of alias analysis that assigns static flow-insensitive regions (disjoint memory areas) to pointer expressions in the program source code in a modular way. That is, if a function parameter has a pointer type, its region can itself be a parameter of the function. So the results of the analysis are local to a function and can be presented as parametric function summaries that are instantiated at call sites by substituting the argument regions in place of the parameter regions. These results can be used to over-approximate the function effects, i.e. the sets of heap locations possibly assigned by each function. The presented analysis is not precise enough to be directly used for the purpose of verification, but it can be made very efficient and can quickly compute sound approximations for functions deep in the call stack. This can be used to iteratively expand the scope of verification by gradually including the code of over-approximated functions based on infeasible counterexamples.

Martin Spießl - Configurable Software Verification based on Slicing Abstractions

Abstraction Slicing is a CEGAR-based software verification technique that is used in different contexts by the software model checkers SLAB and Ultimate Kojak. Based on the predicates gained by an spurious counterexample, states in the abstract model are split and infeasible edges removed. Other CEGAR-based approaches like predicate abstraction and lazy abstraction with interpolants remove infeasible states instead of checking edges for infeasibility.
We implemented basic versions of SLAB and Kojak into the CPAchecker framework. This allows us to compare them to each other as well as to other similar approaches like predicate abstraction or lazy abstraction with interpolants. With optimizations for abstraction slicing similar to adjustable-block encoding we can observe the effect of different block sizes on the performance of the new analyses.

Vitaly Mordan - Towards Complex Specifications in Software Model Checking

The talk is devoted to representing complex specifications in software model checking independently from the analyzed source code. It presents overview of what already have been done in this direction and which problems are still open. Also potential benefits of using the suggested approach instead of weaving specifications in the source code will be demonstrated. In future supporting complex specifications separately from the source code can significantly help to verify real-life software.

11:00 - 11:30 Coffee break
11:30 - 13:00
Ilia Zakharov - Automated Static Verification of GNU C Programs
Ilya Shchepetkov - Extracting Information About Software Build Process and Source Code
Evgeny Novikov - Verification of the Linux Kernel without Loadable Kernel Modules
13:00 - 14:00 Launch
14:00 - 16:00
Manuel Töws - Domination Validation
Vadim Mutilin - Analysis Strategies for Variability Bugs in the Linux Kernel
Anton Vasilyev - SMG: Current State and Future Work
Philipp Wendler - CPAchecker on GitLab, Verifier Web Client
16:00 - 16:30 Coffee break
16:30 - 17:30
Alexey Khoroshilov - Discussion
19:00 Bolshoi Circus