Towards Evaluating Size Reduction Techniques for Software Model Checking

TL;DR

This paper presents a framework for transforming C programs into formal models with various size reduction optimizations, evaluating their impact on model size and verification efficiency.

Contribution

It introduces a flexible framework that incorporates multiple size reduction algorithms for formal models of C programs, enabling tailored optimization strategies.

Findings

Different optimizations are more effective for specific models.

The framework improves verification efficiency by reducing model size.

Multiple algorithms are necessary for optimal size reduction.

Abstract

Formal verification techniques are widely used for detecting design flaws in software systems. Formal verification can be done by transforming an already implemented source code to a formal model and attempting to prove certain properties of the model (e.g. that no erroneous state can occur during execution). Unfortunately, transformations from source code to a formal model often yield large and complex models, making the verification process inefficient and costly. In order to reduce the size of the resulting model, optimization transformations can be used. Such optimizations include common algorithms known from compiler design and different program slicing techniques. Our paper describes a framework for transforming C programs to a formal model, enhanced by various optimizations for size reduction. We evaluate and compare several optimization algorithms regarding their effect on the size of the model and the efficiency of the verification. Results show that different optimizations are more suitable for certain models, justifying the need for a framework that includes several algorithms.