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

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.

slides

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.

slides

slides

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.

slides

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.

slides

slides

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.

slides

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.

slides

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.

slides

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.

slides

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.

slides

slides

slides

slides

slides

slides

Panel discussion devoted to summarization of the topics raised during the workshop, to clarification of user expectations and to writing down action items identified.