Towards Evaluating Size Reduction Techniques for Software Model Checking

Gyula Sallai
(Department of Measurement and Information Systems, Budapest University of Technology and Economics)
Ákos Hajdu
(Department of Measurement and Information Systems, Budapest University of Technology and Economics / MTA-BME Lendület Cyber-Physical Systems Research Group)
Tamás Tóth
(Department of Measurement and Information Systems, Budapest University of Technology and Economics)
Zoltán Micskei
(Department of Measurement and Information Systems, Budapest University of Technology and Economics)

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.

In Alexei Lisitsa, Andrei P. Nemytykh and Maurizio Proietti: Proceedings Fifth International Workshop on Verification and Program Transformation (VPT 2017), Uppsala, Sweden, 29th April 2017, Electronic Proceedings in Theoretical Computer Science 253, pp. 75–91.
Published: 23rd August 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.253.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org