Steinhöfel, Dominic ; Hähnle, Reiner ; Bubel, Richard
eds.: Ogata, Kazuhiro ; Lawford, Mark ; Liu, Shaoying (2016)
A General Lattice Model for Merging Symbolic Execution Branches.
doi: 10.1007/978-3-319-47846-3_5
Conference or Workshop Item, Bibliographie
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 ; Lawford, Mark ; Liu, Shaoying |
| Creators: | Steinhöfel, Dominic ; Hähnle, Reiner ; Bubel, Richard |
| Type of entry: | Bibliographie |
| Title: | A General Lattice Model for Merging Symbolic Execution Branches |
| Language: | German |
| Date: | 2016 |
| Publisher: | Springer International Publishing |
| Book Title: | Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings |
| Series: | Lecture Notes in Computer Science |
| Series Volume: | 10009 |
| DOI: | 10.1007/978-3-319-47846-3_5 |
| URL / URN: | https://doi.org/10.1007/978-3-319-47846-3\_5 |
| 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. |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 08 Mar 2019 15:58 |
| Last Modified: | 08 Mar 2019 15:58 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum