Abstract
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.
Cite
CITATION STYLE
Chalupa, M., & Strejček, J. (2019). Evaluation of Program Slicing in Software Verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11918 LNCS, pp. 101–119). Springer. https://doi.org/10.1007/978-3-030-34968-4_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
