Scheurer, Dominic (2014)
From Trees to DAGs: A General Lattice Model for Symbolic Execution.
Technische Universität Darmstadt
Master Thesis, Bibliographie
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.
| Item Type: | Master Thesis |
|---|---|
| Erschienen: | 2014 |
| Creators: | Scheurer, Dominic |
| Type of entry: | Bibliographie |
| Title: | From Trees to DAGs: A General Lattice Model for Symbolic Execution |
| Language: | English |
| Referees: | Hähnle, Reiner ; Wasser, Nathan ; Bubel, Richard |
| Date: | 2014 |
| Place of Publication: | Darmstadt |
| Event Location: | Darmstadt |
| URL / URN: | https://download.hrz.tu-darmstadt.de/media/FB20/Dekanat/Publ... |
| 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. |
| Identification Number: | TUD-CS-2014-1067 |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 31 Dec 2016 10:40 |
| Last Modified: | 06 Nov 2019 08:07 |
| PPN: | |
| Referees: | Hähnle, Reiner ; Wasser, Nathan ; Bubel, Richard |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum