Evaluation of Program Slicing in Software Verification

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

CHALUPA Marek STREJČEK Jan

Year of publication 2019
Type Article in Proceedings
Conference Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
Web https://link.springer.com/chapter/10.1007%2F978-3-030-34968-4_6
Doi http://dx.doi.org/10.1007/978-3-030-34968-4_6
Keywords program analysis; static program slicing; verification
Description There are publications that consider the use of program slicing in software verification, but we are aware of no publication that thoroughly evaluates the impact of program slicing on the verification process. This paper aims to fill in this gap by providing a comparison of the effect of program slicing on the performance of the reachability analysis in several state-of-the-art software verification tools, namely CPAchecker, DIVINE, KLEE, SeaHorn, and SMACK. The effect of slicing is evaluated on the number of solved benchmarks and running times of the tools. Experiments show that the effect of program slicing is mostly positive and can significantly improve the performance of some tools.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.