4th International Workshop on CPAchecker (CPA '19)

In this talk, we will see the approach to automatic software verification that is implemented in the Ultimate Automizer tool. The approach is based on a new view to programs. In this new view, the focus lies not on program states, instead the focus lies on sequences of statements, which we call traces. We view a program as an automaton whose alphabet consists of the program’s statements. Hence, each program defines a set of traces and we can apply automata-theoretic operations to programs. Ultimate Automizer uses this connection between programs and sets of traces to decompose a program, to prove correctness of the components, and to compose these correctness proofs to a correctness proof for the program.

Model checking is used to automatically verify a model against a specification. In terms of software model checking, this ensures that the program behaves correctly and does what it is supposed to do. The standard approach is to statically analyze a program, construct an abstract model thereof, and finally perform an exhaustive search of the state space in order to determine whether the specification holds. The latter is mostly given in the form of a temporal logic, because this allows to easily express desirable properties of a system, such as e.g. functional correctness, reachability, safety, or liveness. In this talk an approach is presented on how CPAchecker can be utilized to perform software model checking for linear temporal logics (LTL). The main objective lies on analyzing programs written in C to be verified for LTL properties, and in particular, liveness-properties thereof. Generally, this can be done by converting a negated LTL formula into an automaton on infinite words (more specifically, a Büchi automaton), and combine this afterwards with a model of the software program. In CPAchecker, this results in an abstract reachability graph (ARG), that has a finite set of states which can be reached from an initial starting state. The correctness requirement is eventually proven by verifying that there is no set of words left which the ARG accepts, i.e., that the language of the ARG is empty.

Configurable Program Analysis is a theoretical framework, which allows unifying different approaches to program analysis, such as Bounded Model Checking, Predicate Abstraction, Impact, and others. However, an efficient approach for analysis of multithreaded programs - Thread-Modular Analysis - can not be expressed in the classic CPA algorithm, as it operates with partial abstract states. A partial abstract state represents a state of single thread without any information about other threads and can not provide all available transitions at once. The presentation introduces an extension of the CPA framework with a concept of transition abstraction that allows breaking a step forward from an abstract state into separate steps. As a result, several new program analysis approaches including thread-modular ones can be implemented and evaluated within the proposed CPA extension.

The goal of cooperative verification is to combine verification approaches in such a way that they work together to verify a system model. In particular, cooperative verifiers provide exchangeable information (verification artifacts) to other verifiers or consume such information from other verifiers with the goal of increasing the overall effectiveness and efficiency of the verification process. We first give an overview over approaches for leveraging strengths of different techniques, algorithms, and tools in order to increase the power and abilities of the state of the art in software verification. Second, we specifically outline cooperative verification approaches and discuss their employed verification artifacts. We formalize all artifacts in a uniform way, thereby fixing their semantics and providing verifiers with a precise meaning of the exchanged information. Joint work with Heike Wehrheim: https://arxiv.org/pdf/1905.08505

To apply software verification in software-development projects, it must efficiently handle incremental changes in software systems. Incremental verification approaches are designed to tackle this problem. In this talk, I will present work in progress on modular differential software verification, an incremental verification approach based on conditional model checking. In contrast, to existing incremental verification approaches modular differential software verification can be used with arbitrary verification tools and even if a full verification is impossible. The basic idea of modular differential software verification is to first construct a condition that encodes program executions affected by the program modification and then apply (reducer-based) conditional model checking to only verify the affected program executions. I will describe how we build the required condition, report on first experimental results, and discuss current challenges and future steps for modular differential software verification. Keywords: incremental verification, regression verification, conditional model checking

We developed a stand-alone witness validator for C code based on interpretation that is both fast and memory efficient. We decided to trade avoiding overhead in runtime and memory introduced by invoking full-blown model checkers or compilers for reduced performance on larger witnesses and being constrained to precise witnesses.

Amongst other topics, we will look at the switch to Java 11 and discuss whether the issue tracker will be made public.

Symbiotic is a framework that employs fast static analyses with code instrumentation, program slicing, and compiler optimizations to generate a transformed program fitted to the verification of a given property. Additionally, it integrates several verification tools that can be seamlessly run on the generated program. One of these tools is CPAchecker. The talk will describe the background of Symbiotic, the integration of CPAchecker in Symbiotic and our experience with this combination.

The first part of the talk presents achievements of CPAchecher in Linux driver verification project by considering bugs which was found and fixed in the Linux kernels. We take a look on different characteristics like kernel versions, subsystems, consequences, etc. The second part is devoted to discussion of current and future works related to verification of operating systems.

This talk presents a methodology for automatic generation of modification-revealing regression test cases between two program versions, including parameters for adjusting the number of differentiating test cases and the number of preceding program versions taken into account. The test cases are generated using CPAchecker encoded as standard reachability-problems and using on-the-fly path exclusion for multi-test-case generation.

Software verification tools allows both finding complicated errors and proving the correctness of components of large software systems in C language. Such tools are especially demanded in practice at developing complex software systems with a size of hundreds of thousands of lines of C code that must meet the high requirements of reliability and security. To apply verification tools to such software systems, it is necessary to prepare verification tasks, the solution of which is already carried out automatically by verification tools. This report will discuss the tasks that need to be addressed at preparing programs for verification in practice, and the tools for solving them, which are supplied as part of the Klever verification framework designed to reduce the labourness of verification of large software systems.

Symbolic Memory Graphs allow precise reasoning about low-level memory properties of programs. This talk will describe the basics of SMGs including list abstraction and an approach for CEGAR. The current state of SMGs in CPAchecker as well as further plans are presented.

Static verification of memory safety properties is based on making memory model, which precisely reflects features of computer memory. We are using symbolic memory graphs for simulating C memory with ability for pointer arithmetic. This memory model keeps invariants for legal operations by construction. Current report describes graph memory model invariants and optimizations of SMGCPA based on them.

The talk presents perspectives of static verification results visualization. First, a new technique will be presented, which is able to convert a witness (both violation and correctness) into some user friendly format. This technique operates with SV-COMP common witness format, supports all SV-COMP properties (along with CPAchecker property automata) and can process witnesses if needed (for example, filter similar witnesses, if more than one was produced for a given task). It will help to verifier developers to demonstrate produced witnesses to verifier users. Second, the ideas of correctness witnesses visualization will be demonstrated with several examples. Such visualization will show core correctness proof data (such as invariants) in short form, which is more useful for verifier developers, and all covered conditions and lines, which is easy to understand for verifier users. Third, a web-interface for visualization of verification results, which were obtained by BenchExec, will be shown. It groups all results for each run-definition into a single report, which includes found correctness and violation witnesses (in presented user friendly format) and some additional information (such as verifier logs, statistics on consumed resources, coverage of source files, etc.). The user can mark witnesses (for example, as a real bug or an incorrect proof), and such marks will be applied for further reports. This web-interface can be used by software developers for regression verification as well as by verifier developers for SV-COMP tasks