Steinhöfel, Dominic ; Hähnle, Reiner ; Bubel, Richard
Hrsg.: 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
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2016 |
| Herausgeber: | Ogata, Kazuhiro ; Lawford, Mark ; Liu, Shaoying |
| Autor(en): | Steinhöfel, Dominic ; Hähnle, Reiner ; Bubel, Richard |
| Art des Eintrags: | Bibliographie |
| Titel: | A General Lattice Model for Merging Symbolic Execution Branches |
| Sprache: | Deutsch |
| Publikationsjahr: | 2016 |
| Verlag: | Springer International Publishing |
| Buchtitel: | Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings |
| Reihe: | Lecture Notes in Computer Science |
| Band einer Reihe: | 10009 |
| DOI: | 10.1007/978-3-319-47846-3_5 |
| URL / URN: | https://doi.org/10.1007/978-3-319-47846-3\_5 |
| Kurzbeschreibung (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. |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 08 Mär 2019 15:58 |
| Letzte Änderung: | 08 Mär 2019 15:58 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum