arXiv subjects

Marie-Christine Jakobs

Publications and source records attributed to Marie-Christine Jakobs.

7 recordsLinked to original sources

arXiv2026

Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement

Automatic software verification is a valuable means for software quality assurance. However, automatic verification and in particular software model checking can be time-consuming, which hinders their practical applicability e.g., the use in continuous integration. One solution to address the issue is to reduce the response time of the verification procedure by leveraging today's multi-core CPUs. In this paper, we propose a solution to parallelize trace abstraction, an abstraction-based approach to software model checking. The underlying idea of our approach is to parallelize the abstraction refinement. More concretely, our approach analyzes different traces (syntactic program paths) that could violate the safety property in parallel. We realize our parallelized version of trace abstraction in the verification tool Ulti mate Automizer and perform a thorough evaluation. Our evaluation shows that our parallelization is more effective than sequential trace abstraction and can provide results significantly faster on many time-consuming tasks. Also, our approach is more effective than DSS, a recent parallel approach to abstraction-based software model checking.

cs.LO↗

arXiv2024

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)

This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k -induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.

cs.SE↗

arXiv2024

Parallel Program Analysis on Path Ranges

Symbolic execution is a software verification technique symbolically running programs and thereby checking for bugs. Ranged symbolic execution performs symbolic execution on program parts, so called path ranges, in parallel. Due to the parallelism, verification is accelerated and hence scales to larger programs. In this paper, we discuss a generalization of ranged symbolic execution to arbitrary program analyses. More specifically, we present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel. Our approach in particular allows to run different analyses on different program parts. We have implemented this generalization on top of the tool CPAchecker and evaluated it on programs from the SV-COMP benchmark. Our evaluation shows that verification can benefit from the parallelisation of the verification task, but also needs a form of work stealing (between analyses) as to become efficient

cs.SE↗

arXiv2023

Incorporating Data Dependencies and Properties in Difference Verification with Conditions (Technical Report)

Software changes frequently. To efficiently deal with such frequent changes, software verification tools must be incremental. Most of today's approaches for incremental verification consider one specific verification approach. One exception is difference verification with conditions recently proposed by Beyer et al. Its underlying idea is to determine an overapproximation of those modified execution paths that may cause a new property violation, which does not exist in the unchanged program, encode the determined paths into a condition, and use the condition to restrict the verification to the analysis of those determined paths. To determine the overapproximation, Beyer et al. propose a syntax-based difference detector that adds any syntactical path of the modified program that does not exist in the original program into the overapproximation. This paper provides a second difference detector diffDP, which computes a more precise overapproximation by taking data dependencies and program properties into account when determining the overapproximation of those modified execution paths that may cause a new property violation. Our evaluation indeed shows that our more precise difference detector improves the effectiveness and efficiency of difference verification with condition on several tasks.

cs.LO↗

arXiv2021

PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)

Refactorings must not alter the program's functionality. However, not all refactorings fulfill this requirement. Hence, one must explicitly check that a refactoring does not alter the functionality. Since one rarely has a formal specification of the program's behavior, we utilize the original program as functional specification. Then, we check whether the original and refactored program are functionally equivalent. To this end, we apply a common idea and reduce equivalence checking to program verification. To increase efficiency, our equivalence checker PEQcheck constructs one verification task per refactored code segment instead of one per function as typically done by prior work. In addition, PEQcheck considers the context of the code segments. For instance, only variables that are modified and live are required to be equivalent and read-only variables may be shared between original and refactored code segments. We show that PEQcheck is sound.Moreover, our evaluation testifies that the localized and context-aware checking performed by \peqcheck can indeed be beneficial.

cs.LO↗

arXiv2017

Predicting Rankings of Software Verification Competitions

Software verification competitions, such as the annual SV-COMP, evaluate software verification tools with respect to their effectivity and efficiency. Typically, the outcome of a competition is a (possibly category-specific) ranking of the tools. For many applications, such as building portfolio solvers, it would be desirable to have an idea of the (relative) performance of verification tools on a given verification task beforehand, i.e., prior to actually running all tools on the task. In this paper, we present a machine learning approach to predicting rankings of tools on verification tasks. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for verification tasks. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy. In particular, our method outperforms a recently proposed feature-based approach of Demyanova et al. (when applied to rank predictions).

cs.LG↗

arXiv2016

Deriving approximation tolerance constraints from verification runs

Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing for hardware which only carries out "approximately correct" calculations. For software verification, this challenges the validity of verification results for programs run on approximate hardware. In this paper, we present a novel approach to examine program correctness in the context of approximate computing. In contrast to all existing approaches, we start with a standard program verification and compute the allowed tolerances for AC hardware from that verification run. More precisely, we derive a set of constraints which - when met by the AC hardware - guarantees the verification result to carry over to AC. Our approach is based on the framework of abstract interpretation. On the practical side, we furthermore (1) show how to extract tolerance constraints from verification runs employing predicate abstraction as an instance of abstract interpretation, and (2) show how to check such constraints on hardware designs. We exemplify our technique on example C programs and a number of recently proposed approximate adders.

cs.SE↗