Steinhöfel, Dominic ; Hähnle, Reiner ; Bubel, Richard
Ogata, Kazuhiro ; Lawford, Mark ; Liu, Shaoying (eds.) (2016):
A General Lattice Model for Merging Symbolic Execution Branches.
In: Lecture Notes in Computer Science, 10009, In: Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings, pp. 57-73,
Springer International Publishing, DOI: 10.1007/978-3-319-47846-3_5,
[Conference or Workshop Item]

Abstract

Symbolic execution is a software analysis technique that has been used with success in the past years in program testing and verification. A main bottleneck of symbolic execution is the path explosion problem: the number of paths in a symbolic execution tree is exponential in the number of static branches of the executed program. Here we put forward an abstraction-based framework for state merging in symbolic execution. We show that it subsumes existing approaches and prove soundness. The method was implemented in the verification system KeY. Our empirical evaluation shows that reductions in proof size of up to 80 % are possible by state merging when applied to complex verification problems; new proofs become feasible that were out of reach so far.

Send an inquiry

Show editorial Details