TU Darmstadt / ULB / TUbiblio

A General Lattice Model for Merging Symbolic Execution Branches

Steinhöfel, Dominic and Hähnle, Reiner and Bubel, Richard
Ogata, Kazuhiro and Lawford, Mark and Liu, Shaoying (eds.) (2016):
A General Lattice Model for Merging Symbolic Execution Branches.
In: Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings, Springer International Publishing, In: Lecture Notes in Computer Science, DOI: 10.1007/978-3-319-47846-3_5, [Online-Edition: https://doi.org/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.

Item Type: Conference or Workshop Item
Erschienen: 2016
Editors: Ogata, Kazuhiro and Lawford, Mark and Liu, Shaoying
Creators: Steinhöfel, Dominic and Hähnle, Reiner and Bubel, Richard
Title: A General Lattice Model for Merging Symbolic Execution Branches
Language: German
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.

Title of Book: Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings
Series Name: Lecture Notes in Computer Science
Volume: 10009
Publisher: Springer International Publishing
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Date Deposited: 08 Mar 2019 15:58
DOI: 10.1007/978-3-319-47846-3_5
Official URL: https://doi.org/10.1007/978-3-319-47846-3\_5
Export:

Optionen (nur für Redakteure)

View Item View Item