Static verification tools like CPAchecker can grant users invaluable information on programs safety. In my talk I will present what is necessary to make things work, what was implemented in various verification frameworks thus far and what we have been doing towards automated static verification of C programs.

slides

The talk is devoted to a problem of increasing efficiency of verification in real-life conditions. Two main aspects to be considered are the need to verify many properties of target software and the need to verify each new version of the software. The approaches to handle such situations more efficiently and results of experiments will be presented. In addition, the talk discusses changes for BenchExec required to support the suggested approaches as well as a new SV-COMP 'multi-property' demo-category.

The talk presents overview of issues, features and perspectives of application of CPAchecker for Linux driver verification.

SystemC is widely used in hardware/software codesign. Although it is also used for the design of safety-critical applications, existing formal verification techniques for SystemC are still hardly used in industrial practice. The main reasons for this are scalability issues, the lacking support for many practically relevant SystemC language constructs, and that counter-examples are not always easy to use for debugging. In this talk, I present an approach for the formal verification of SystemC designs using the CPAchecker. I show how we automatically transform given SystemC designs into C code that can be verified with the CPAchecker, and present some preliminary experimental results from an Anti-Slip Regulation and Anti-Lock Braking system (ASR/ABS).

The LLVM compiler infrastructure provides the LLVM code representation, an assembler-like, typed intermediate language in SSA form and with a clear structure. Because of its perks, LLVM is used in many modern software analysis tools. CPAchecker, on the other hand, only supports the languages C and Java. Since it is hard to translate LLVM back to C, it is hard to benefit from combinations between CPAchecker and such other tools. To make tool combinations possible, we implement a frontend for LLVM in CPAchecker. This frontend maps LLVM to C semantics internally, providing the full suite of CPAchecker analyses for use with LLVM bitcode. The talk will give an overview over LLVM and the current state of its frontend implementation in CPAchecker.

Determination of false positives and real bugs is an integral part of any verification process carried out with static verification tools. Today a violation witness is the only artifact that allows an expert to understand an error path provided by a static verification tool but at the same time, it is by design not intended for manual consideration. The talk presents problems and potential solutions for improving manual analysis of violation witnesses.

Due to the increasing importance of witnesses, e.g. in the SV-COMP, verification tools substantiate their answers with witnesses. In this talk, we are interested in the question: how to build a correctness witness when the verification effort is split among multiple analyses, which is often used when a single analysis would fail or is inefficient on some program parts. We present PARTPW, our answer to that question, and report on first experiments.

slides

After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. Several of the most widely used approaches for software model checking are based on solving first-order-logic formulas over predicates using SMT solvers, e.g., predicate abstraction, bounded model checking, k-induction, and lazy abstraction with interpolants. We define a configurable framework for predicate-based analyses that allows expressing each of these approaches and is based on CPAchecker's core concept, configurable program analysis. This unifying framework highlights the differences between the approaches, producing new insights, and facilitates research of further algorithms and their combinations. To pinpoint both the similarities and differences between the approaches, we exercise the approaches on a running example. Finally, we use the implementation of our unifying framework for predicate analysis in CPAchecker to perform an experimental study. We evaluate the effect of varying the SMT solver and the way program semantics are encoded in formulas across several verification algorithms and find that these technical choices can significantly influence the results of experimental studies of verification approaches. This is valuable information for both researchers who study verification approaches as well as for users who apply them in practice and motivates upcoming changes in CPAchecker's default configurations.

slides

Software model checkers can generate high-quality test cases from counterexamples of a reachability analysis. However, naively invoking a model checker for each test goal in isolation does not scale to large programs as a repeated construction of an abstract program model is expensive. We therefore propose a novel test-generation technique that allows for configurable partitioning and simultaneous processing of multiple test goals in one reachability analysis. To this end, we extend multi-property verification in order to control the computational overhead for tracking multi-goal reachability information. Our technique employs symbolic path sensitivity which is orthogonal to data-flow analysis for eliminating infeasible program paths. We instantiate our approach with predicate-abstraction-based program analysis in the model-checking framework CPAchecker. Our experiments show that (1) processing all test goals at once dramatically improves performance of test generation in case of small and medium program sizes, and (2) in case of large programs, there seems to be a critical test-goal set size above which the benefits of multi-goal processing are outweighed by the additional overhead. These promising results encourage us to further investigate automatic test-goal set partitioning strategies.

slides

SMGCPa is a CPAchecker-based analysis for verifying memory safety properties of C programs. The talk presents recent improvements implemented in SMGCPA and demonstrates how they affect results of SMGCPA application for analysis of Linux kernel code. A list of open problems and possible future directions are discussed.

slides

Information Flow Analysis aims at detecting illegal flows of information between program entities. In this talk, I present a configurable over-approximation technique based on dependency analyses to compute information flow analysis results for general security policies. These results can be either generic, i.e. independent of the underlying policy, or in a dependent way tailored to a security policy. I will present general security policies, present the analyses and how they work in general. I will conclude with investigations over refinement relations between policies allowing reuse of analyses results computed for one security concern for another one. These refinements depends on concrete program entities and a big part of the computation can be precomputed leading to efficient refinement checks.

Scalability of existing verifiers of multithreaded software leaves much to be desired. Precise approaches fail to handle real-life software, while lightweight techniques suffer from false alarms and missed bugs. There are also ideas of combinations, e.g. where lightweight analysis provides some hints to a main precise analysis (SMACK+Corral). The talk presents a CPAchecker-based approach that makes an attempt to be adjustable for keeping the balance between speed and accuracy. Also the approach can be used as a lightweight frontend for more heavyweight analysis.

This talk gives an introduction to the concept of Slicing Abstractions like it can be found in the software model checkers SLAB or Ultimate Kojak. It points out similarities and differences to other counterexample-guided abstraction refinement strategies and addresses the question as to how it can be integrated into the CPAchecker framework.

slides

Block-abstraction memoization (BAM) aims towards a scalable analysis for large programs by dividing a program into blocks that are analyzed separately. It can be used as part of a CEGAR approach to improve the efficiency of the analysis by learning and only tracking the relevant facts. Until now, the refinement process for BAM was insufficient for several programs and caused large computational overhead or even endless loops. We explored that the reason for this problem is not based on bugs in the implementation, but a fundamental problem with the theory of BAM, i.e., the original definition of the lazy refinement in BAM that was too weak and left too much space for interpretation. We present a correct and sound solution for the problem, which is based on a copy-on-write approach during the refinement, instead the previous in-place update of the reached state space.

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.

MindMap