A Modular Program-Transformation Framework for Reducing Specifications to Reachability

TL;DR

This work tackles the high engineering cost of software verification by introducing a modular transformation framework that reduces various specifications to reachability via instrumentation automata applied to the input program. By separating the verification algorithm from specification handling, the approach enables any C-reachability verifier to process properties like termination, no-overflow, and memory cleanup as preprocessing steps, using a formal CFA/IA pipeline with sequentialization and instrumentation operators. Empirical results on SVCOMP24 indicate that transformed reachability verifiers can be competitive with native tools for several specifications and, in some cases, even surpass them, while offering clear modularity and reusability advantages. The framework is open-source, supports general expressiveness (including explicit liveness transformations), and points to future extensions to broaden the set of verifiable properties and interfaces for user-defined instrumentation.

Abstract

Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on reachability properties, or invest the time to implement known transformations from the given specification to reachability on their internal representations. To improve this situation, we provide transformations as stand-alone components, modifying the input program instead of the internal representation, enabling their usage as a preprocessing step by other verifiers. This way, we separate two concerns: improving the performance of reachability analyses and implementing efficient transformations of arbitrary specifications to reachability. We implement the transformations in a framework that is based on instrumentation automata, inspired by the BLAST query language. In our initial study, we support three important concrete specifications for C programs: termination, no-overflow, and memory cleanup. Moreover, we discuss the broader expressiveness of our framework and show how general liveness properties can be transformed to reachability. We demonstrate the effectiveness and efficiency of our transformations by comparing verifiers that support the specifications natively with verifiers for reachability applied on the transformed programs. The results are very promising: Our transformations can extend existing verifiers to be effective on specifications that they do not support natively, and that the efficiency is often similar to verifiers that natively support the considered specifications.

Figures (12)

• Figure 1: An example program (left) with a corresponding CFA (right)
• Figure 2: Workflow of the program transformation
• Figure 3: An example IA (left) and the corresponding CFA after sequentialization with the CFA from \ref{['fig:background:running-example']} (right)
• Figure 4: An example of an instrumented program
• Figure 5: An excerpt of the IA for the no-overflow property