Title: Towards Evaluating Size Reduction Techniques for Software Model Checking,
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.