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.
10009In: Lecture Notes in Computer Science, 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, pp. 57-73, 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: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum