Scheurer, Dominic (2014)
From Trees to DAGs: A General Lattice Model for Symbolic Execution.
Technische Universität Darmstadt
Masterarbeit, Bibliographie
Kurzbeschreibung (Abstract)
Symbolic Execution is a precise static program analysis technique for software testing and verification. In the course of the analysis, programs are transformed into symbolic execution trees containing up to exponentially many branches in the number of branch points. We address this so-called “path explosion problem” in the context of program verification by proposing a general lattice-based framework for join operations that allows for the merging of branches during symbolic execution. Several concrete join techniques are presented as instances of this framework and are implemented for the deductive verification system KeY . We show that our operations indeed reduce the number of states and branches significantly for certain examples, and apply a join technique to information flow analysis in a short case study to demonstrate that state joining can increase the precision of analyses in principle.
| Typ des Eintrags: | Masterarbeit |
|---|---|
| Erschienen: | 2014 |
| Autor(en): | Scheurer, Dominic |
| Art des Eintrags: | Bibliographie |
| Titel: | From Trees to DAGs: A General Lattice Model for Symbolic Execution |
| Sprache: | Englisch |
| Referenten: | Hähnle, Reiner ; Wasser, Nathan ; Bubel, Richard |
| Publikationsjahr: | 2014 |
| Ort: | Darmstadt |
| Veranstaltungsort: | Darmstadt |
| URL / URN: | https://download.hrz.tu-darmstadt.de/media/FB20/Dekanat/Publ... |
| Kurzbeschreibung (Abstract): | Symbolic Execution is a precise static program analysis technique for software testing and verification. In the course of the analysis, programs are transformed into symbolic execution trees containing up to exponentially many branches in the number of branch points. We address this so-called “path explosion problem” in the context of program verification by proposing a general lattice-based framework for join operations that allows for the merging of branches during symbolic execution. Several concrete join techniques are presented as instances of this framework and are implemented for the deductive verification system KeY . We show that our operations indeed reduce the number of states and branches significantly for certain examples, and apply a join technique to information flow analysis in a short case study to demonstrate that state joining can increase the precision of analyses in principle. |
| ID-Nummer: | TUD-CS-2014-1067 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 31 Dez 2016 10:40 |
| Letzte Änderung: | 06 Nov 2019 08:07 |
| PPN: | |
| Referenten: | Hähnle, Reiner ; Wasser, Nathan ; Bubel, Richard |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum