Click on the title of a talk to read the abstract.
The program is also available as PDF.
Thursday, Sept. 22, 2016
9:00–10:30 Session 1: Perspectives
CPAchecker and Linux Driver Verification
Alexey Khoroshilov
(ISP RAS, Russia)
The talk presents experience of usage CPAchecker in Linux Driver Verification program, discusses open questions and future directions.
Bringing Formal Verification Closer to Practicing Engineers: The mbeddr Approach
Daniel Ratiu
(Siemens, Germany)
Despite its huge potential, formal verification is currently not used in the daily software development practice. Engineers regard formal techniques as expert tools and find the overhead of using them to be too big for their needs. In this talk I will present the common challenges which formal verification tools must face in order to be accepted in practice. I will describe our approach to integrate formal analyses in the mbeddr development environment and the use of domain specific languages in order to ease the specification of environments, of verification conditions and the understanding the verification results. I will present our experience with integrating CBMC and other formal verification technology in mbeddr and sketch the possible ways in which CPAchecker could enhance the verification stack of mbeddr.
11:00–12:00 Session 2: Infrastructure
CPAchecker: Towards Large-Scale Bug Discovery
George Karpenkov
(VERIMAG, France)
Despite significant advances during the last decade,
formal methods research is largely ignored by
software engineering community.
Almost all of the high-profile security bugs which
were discovered automatically over the last couple of
years were discovered using fuzzers.
Apart from excellent work done by the LDV project,
very few people use CPAchecker to analyze real,
non-academic datasets.
In this talk we highlight missing (and existing)
bits of CPAchecker infrastructure required
for application to industrial codebases,
and we discuss the future work required to
make such an application practical.
Benchmarking with Containers
Philipp Wendler
(University of Passau, Germany)
Benchmarking is a widely-used method
in experimental computer science,
in particular,
for the comparative evaluation of tools and algorithms.
We identify a set of requirements that are indispensable
for reproducible benchmarking and reliable resource measurement of time and memory usage
of automatic solvers, verifiers, and similar tools,
and discuss limitations of existing methods and benchmarking tools.
Fulfilling these requirements in a benchmarking framework
is complex and can (on Linux) currently only be done
by using the cgroup and namespace features of the kernel.
We developed BenchExec, a ready-to-use, tool-independent, and free implementation
of a benchmarking framework that fulfills all presented requirements,
making reproducible benchmarking and reliable resource measurement easy.
Our framework is
able to work with a wide range of different tools
and has proven its reliability and usefulness in
the International Competition on Software Verification,
and is used by several research groups to ensure reliable benchmarking.
slides
13:30–15:00 Session 3: Improvements and Experiments
Several Recent Experiments with Predicate Analysis
Mikhail Mandrykin
(ISP RAS, Russia)
The talk presents the results of several recent and mostly rather small
experiments with current implementation of predicate CPA and its c-to-formula
conversion component. The experiments were mainly done by bachelor and master
students at ISP RAS (Anton Volkov and Alexey Romanov) and involved some
modification of the current predicate CPA implementation with experimental
evaluation on some typical LDV verification tasks. The experiments were the
following:
-- Implementing "Busrtall\&Bornat" memory model (essentially, one
uninterpreted function per structure field) in c-to-formula converter with
pointer aliasing. (Anton Volkov)
-- Computing path formulas on demand. Applicable only when Predicate CPA is
used in combination with some other CPA (normally, explicit value analysis).
The idea is to run composite analysis with dummy predicate CPA abstract states
taking no time to compute and only start building actual path formulas on the
first refinement (first failed refinement of the other analysis). (Alexey
Romanov)
-- Excluding explicit value predicates (of the form 'var = number') for
variables whose values are explicitly known by the value CPA from predicate
CPA precision coupled with injecting the value analysis results into path
formulas. (Alexey Romanov)
-- New implementation of deferred allocation tracking. (Mikhail Mandrykin)
And also several experiments that required practically no implementation
effort:
-- Limiting the number of memory allocations on a path (unsound)
-- Using Cartesian abstraction and whole interpolants (without atom
extraction)
Further Development of Methods for Verifying Several Properties at Once
Vitaly Mordan
(ISP RAS, Russia)
Static verification of several properties at once has a major potential, which already was shown in multi-aspect verification and on-the-fly decomposition of specification methods. This talk is dedicated to more practical aspects of using both methods for optimizing their efficiency and effectiveness.
At first, two methods for formalization of checked properties will be considered: instrumentation and specification automata. In order to compare both methods all LDV Tools properties (including complex ones, which are generated by some template) were formalized as specification automata and evaluated on separated verification of properties. This experiment has helped to reveal advantages and drawbacks of both methods.
Second, further development of multi-aspect verification method will be presented. Internal and external relaunches in conditional multi-aspect verification will be evaluated in terms of different ways for combination of several verification algorithms. Also the dependence between specified internal parameters and verification results will be shown, which more globally can be seen as dependence between implicit limitations and quality of verification.
After that, a sequential combination of multi-aspect verification and on-the-fly decomposition of specification will be introduced. In general case both multi-aspect verification and on-the-fly decomposition of specification methods have their own strengths and weaknesses. Their sequential combination is aimed at uniting their strengths and at minimizing the influence of their weaknesses. This combination in general case operates with different verifiers, prepares different verification tasks for them and corrects final verdicts based on different factors, which take into account all suggested heuristics of both methods.
At last, the dependence between the number of checked properties and verification results will be described. On the one hand, ideally efficiency of verifying several properties should increase proportionally to the number of properties. On the other hand, increase the number of properties may lead to decrease of efficiency due to many reasons (such as overhead costs and heuristics). Also verifying different number of properties will help to evaluate multi-aspect verification, on-the-fly decomposition of specification and their sequential combination.
15:30–17:00 Session 4: Reuse of Verification Results and Concurrency
Our Reuse of the Abstract Reachability Graph
Marie-Christine Jakobs
(University of Paderborn, Germany)
In this talk, I will introduce three different scenarios in which we make use of an abstract reachability graph constructed during the verification process. First, I briefly present how we check if a program which is proven safe under standard hardware remains if some of the instructions are executed by non-standard hardware, e.g., approximate hardware or customized hardware. The main part of
my talk focuses on efficient reverification of a program. I discuss two configurable frameworks, the programs from proofs framework and the configurable program certification framework. The programs from proofs approach uses the ARG to transform the program into a program whose verification is simpler. In contrast, the configurable program certification framework stores (parts of) the ARG nodes in a clever way to support an efficient reverification. At last, I shortly illustrate one opportunity to continue to test the unverified program paths after an incomplete verification run.
Extension of CPA Approach for Efficient Analysis of Parallel Programs
Pavel Andrianov
(ISP RAS, Russia)
Multi-threaded programs may be analyzed with CPA approach, if it represents a well-known approach with interleavings: an abstract domain is a Cartesian product of abstract domains of single threads. This technique requires a lot of resources. The proposed extension of CPA approach is based on a new kind of transfer - transfer in environment. The extended approach produces false alarms as the environment of a thread (the other threads) are not analyzed precisely, but requires much less resources.
A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker
Karlheinz Friedberger
(University of Passau, Germany)
There are several software model checkers for verifying multi-threaded
programs. Until recently, the program verification framework
CPAchecker lacked direct support for multi-threaded programs.
We introduce a new configurable program analysis that allows to verify
multi-threaded programs with a bounded number of threads. We present
the simple and yet efficient implementation into the existing framework,
which is already competitive on a large benchmark set. Our implementation
can be combined with several existing analyses in CPAchecker,
like value analysis, interval analysis or BDD analysis. The new analysis is
modular and can be used, for example, to verify reachability properties
as well as to detect deadlocks in the program.
The talk includes an evaluation of the benefit of some optimization
steps (e.g. changing the iteration order of the reachability algorithm or
applying partial order reduction) as well as the comparison with other
state-of-the-art tools for verifying multi-threaded programs.
slides
18:00 Workshop Dinner
Our workshop dinner will take place in the Greek restaurant
''Akropolis Athen''
(Rudolf-Guby-Str. 1),
which is located very close to the university campus.
Friday, Sept. 23, 2016
9:00–10:30 Session 5: Configurable Program Analyses
SMT-Based Software Model Checking
Matthias Dangl
(University of Passau, Germany)
After many years of successful development of new algorithms for software model checking, there is a need to consolidate the knowledge about the different algorithms and approaches. This paper gives a coarse overview in terms of effectiveness and efficiency of four algorithms. We compare the following different "schools of thought" of algorithms: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those algorithms are well-known and successful in software verification. They have in common that they are based on SMT solving as the back-end technology, using the theories of uninterpreted functions, bit vectors, and floats as underlying theory. All four algorithms are implemented in the verification framework CPAchecker. Thus, we can present an evaluation that really compares only the core algorithms, and keeps the design variables such as parser front end, SMT solver, used theory in SMT formulas, etc. constant. We evaluate the algorithms on a large set of verification tasks, and discuss the conclusions.
slides
Effective Approaches to Abstraction Refinement for an Explicit-Value Analysis
Stefan Löwe
(University of Passau, Germany)
This talk presents various techniques that aim at enabling more effective
and more efficient approaches for automatic software verification.
First, we briefly describe the design and implementation of the value analysis,
an analysis for automatic software verification that tracks state information concretely,
and which is the main type of analysis featured in this talk.
This plain value analysis leads to an efficient verification process
for many verification tasks, but at the same time, often falls prey to state-space explosion.
To mitigate this effect we propose to incorporate CEGAR and interpolation into the value domain.
We show that with proper optimizations to the CEGAR and interpolation technique,
this novel approach becomes a competitive for automatic software verification.
With the availability of competitive CEGAR-based analyses for the value domain, the predicate domain,
and the combination thereof, we then introduce the notion of infeasible sliced prefixes.
This technique adds choice to the CEGAR loop and enables guided refinement selection,
a concept that may lead to major improvements in verification effectiveness and verification efficiency for any analysis based on CEGAR.
slides
11:00–12:00 Session 6: Memory Safety
Checking Memory Safety with SMGCPA
Anton Vasilyev
(ISP RAS, Russia)
In this talk, I will provide overview of SMG algorithm and detectable error classes, accuracy and model abstraction requirements for Linux kernel memory verification, current development status and verification results.
13:30–15:30 Session 7: Algorithms and Theories
Augmenting Predicate Analysis with Auxiliary Invariants
Thomas Stieglmaier
(University of Passau, Germany)
This talk presents several ways how invariants can be used in a
predicate analysis. We discuss different strategies for generating
invariants, as well as approaches to safely use these invariants for
enhancing predicate analyses. Based on the implementation in CPAchecker
we show examples where invariants are useful and how their usage
influences the analysis. Our best configuration uses two analyses in
parallel and is based on another contribution of this work: an algorithm
for concurrent execution of analyses which allows the used analyses to
communicate via reached sets.
slides
Towards Unbounded Heap Support for Predicate Analysis using SMT Arrays
Stephan Lukasczyk
(University of Passau, Germany)
With this Bachelor thesis, we extended CPAchecker's predicate analysis
with a formula encoding using the SMT theory of arrays to model the
program's heap accesses. In order to evaluate this approach, we
implemented the formula conversion in CPAchecker and ran it with four
different SMT solvers: MathSAT5, Princess, SMTInterpol, and Z3.
Overall, this approach can prove less programs than the existing
approach using uninterpreted functions due to the higher complexity of
solving array formulae, but it can prove more programs with larger
array sizes. We will also give an outlook of work done by others
after finishing the thesis.
slides
Implementing Termination Analysis using Configurable Software Verification
Sebastian Ott
(University of Passau, Germany)
This talk presents a termination algorithm based on a reachability
analysis and a component that synthesises termination and
non-termination arguments from potential error paths. The implementation
of the algorithm in CPAchecker is evaluated on verification tasks from
the SV-COMP. Our implementation achieves correct results for many
programs, but is not as efficient as other tools if programs with
pointers are analysed.
slides
16:00–17:00 Session 8: Open Problems
Directing CPAchecker State Exploration with the Help of Hints from a Linux Driver Environment Model for More Efficient Bug Finding
Ilia Zakharov
(ISP RAS, Russia)
Verification of Linux device drivers with help of CPAchecker requires addiction of an environment model to each driver source code. An environment model implements scenarios of a driver callbacks execution taking into account restrictions on an order of callback execution, its parameters and context of the execution. Since drivers are event-driven software, a precise environment model can contain too many paths to check which often leads to inability of CPAchecker to prove driver correctness within reasonable amount of time. But for a bug finding in order to obtain better results it is enough to check correctness of particular paths first and only then continue verification of the rest driver if an error has not been found. This talk is dedicated to the question how an environment model can help CPAchecker to choose path more efficiently to find a bug within a reasonable time.
17:00–17:30 Session 9: Closing, Discussion, and Outlook