Refine
Year of publication
- 2017 (2)
Document Type
- Doctoral Thesis (2)
Language
- English (2)
Has Fulltext
- yes (2)
Is part of the Bibliography
- no (2)
Keywords
- Programmverifikation (2) (remove)
Institute
Software model checking is a successful technique for automated program verification. 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. This unifying framework highlights the differences between the approaches, producing new insights, and facilitates research of further algorithms and their combinations, as witnessed by several research projects that have been conducted on top of this framework. In addition to this theoretical contribution, we provide a mature implementation of our framework in the software verifier that allows applying all of the mentioned approaches to practice. This implementation is used by other research groups, e.g., to find bugs in the Linux kernel, and has proven its competitiveness by winning gold medals in the International Competition on Software Verification.
Tools and approaches for software model checking like our predicate analysis are typically evaluated using performance benchmarking on large sets of verification tasks. We have identified several pitfalls that can silently arise during benchmarking, and we have found that the benchmarking techniques and tools that are used by many researchers do not guarantee valid results in practice, but may produce arbitrarily large measurement errors. Furthermore, certain hardware characteristics can also have nondeterministic influence on the measurements. In order to being able to properly evaluate our framework for software verification, we study the effects of these hardware characteristics, and define a list of the most important requirements that need to be ensured for reliable benchmarking. We present as solution an open-source benchmarking framework BenchExec, which in contrast to other benchmarking tools fulfills all our requirements and aims at making reliable benchmarking easy. BenchExec was already adopted by several research groups and the International Competition on Software Verification.
Using the power of BenchExec we conduct an experimental evaluation of our unifying framework for predicate analysis. We study 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. Our comprehensive study of 120 different configurations would not have been possible without our highly flexible and configurable unifying framework for predicate analysis and shows that the latter is a valuable base for conducting experiments. Furthermore, we show using a comparison against top-ranking verifiers from the International Competition on Software Verification that our implementation is highly competitive and can outperform the state of the art.
This thesis presents various techniques that aim at enabling more effective and more
efficient approaches for automatic software verification.
After a brief motivation why automatic software verification is getting ever more
relevant, we continue with detailing the formalism used in this thesis and on the
concepts it is built on.
We then describe the design and implementation of the value analysis, an analysis
for automatic software verification that tracks state information concretely. From
a thorough evaluation based on well over 4 000 verification tasks from the latest
edition of the International Competition on Software Verification (SV-COMP), we
learn that this plain value analysis leads to an efficient verification process for many
verification tasks, but at the same time, fails to solve other verification tasks due
to state-space explosion. From this insight we infer that some form of abstraction
technique must be added to the value analysis in order to also allow the successful
verification of large and complex verification tasks.
As a solution, we propose to incorporate counterexample-guided abstraction refinement (CEGAR) and interpolation into the value domain. To this end, we design
a novel interpolation procedure, that extracts from infeasible counterexamples interpolants for the value domain, allowing to form a precision strong enough to exclude
these infeasible counterexamples, and to make progress in the CEGAR loop. We
then describe several optimizations and extensions to these concepts, such that the
value analysis with CEGAR becomes competitive for automatic software verification.
As the next step, we combine the value analysis with CEGAR with a predicate
analysis, to obtain a more precise and efficient composite analysis based on CEGAR.
This composite analysis is indeed on a par with the world’s leading software verification tools, as witnessed by the results of SV-COMP’13 where this approach achieved
the 2 nd place in the overall ranking.
After having available competitive CEGAR-based analyses for the value domain,
the predicate domain, and the combination thereof, we then turn our attention to
techniques that have the goal to make all these CEGAR-based approaches more
successful. Our first novel idea in this regard is based on the concept of infeasible
sliced prefixes, which allow the computation of different precisions from a single
infeasible counterexample. This adds choice to the CEGAR loop, while without this
enhancement, no choice for a specific precision, i. e., a specific refinement, is possible.
In our evaluation we show, for both the value analysis and the predicate analysis,
that choosing different infeasible sliced prefixes during the refinement step leads to
major differences in verification effectiveness and verification efficiency.
Extending on the concept of infeasible sliced prefixes, we define several heuristics
in order to precisely select a single refinement from a set of possible refinements. We
make this new concept, which we refer to as guided refinement selection, available
to both the value and predicate analysis, and in a large-scale evaluation we try to
answer the question which selection technique leads to well suited abstractions and
thus, to a more effective verification process. Additionally, we present the idea of
inter-analysis refinement selection, where the refinement component of a composite
analysis may decide which of its component analyses is best to be refined, and in yet
another evaluation we highlight the positive effects of this technique.
Finally, we present the results of SV-COMP’16, where the verifier we contributed
and which is based on the concepts and ideas presented in this thesis achieved the
1 st place in the category DeviceDriversLinux64.