TU Darmstadt / ULB / TUbiblio

From Trees to DAGs: A General Lattice Model for Symbolic Execution

Scheurer, Dominic (2014):
From Trees to DAGs: A General Lattice Model for Symbolic Execution.
Department of Computer Science, Software Engineering, [Master Thesis]

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
Title: From Trees to DAGs: A General Lattice Model for Symbolic Execution
Language: English
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.

Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Event Location: Darmstadt
Date Deposited: 31 Dec 2016 10:40
Identification Number: TUD-CS-2014-1067
Referees: Hähnle, Reiner and Wasser, Nathan and Bubel, Richard
Related URLs:
Export:

Optionen (nur für Redakteure)

View Item View Item