HOME | DEUTSCH | IMPRESSUM | KIT

Conference Papers: On Temporal Path Conditions in Dependence Graphs

[lochbihler07scam]Andreas Lochbihler, Gregor Snelting, On Temporal Path Conditions in Dependence Graphs, 7th IEEE Working Conference on Source Code Analysis and Manipulation (SCAM 2007), pp. 49--58, IEEE, Maison Internationale, Paris, France, September 2007.

Abstract

Program dependence graphs are a well-established device to represent possible information flow in a program. Path conditions in dependence graphs have been proposed to express more detailed circumstances of a particular flow; they provide precise necessary conditions for information flow along a path or chop in a dependence graph. Ordinary boolean path conditions however cannot express temporal properties, e.g. that for a specific flow it is necessary that a specific condition holds, and later another specific condition holds. In this contribution, we introduce temporal path conditions, which extend ordinary path conditions by temporal operators in order to express temporal dependencies between conditions for a flow. We present motivating examples, generation and simplification rules, and a case study. Applying model checking generates "witnesses" for a specific flow. We prove the following soundness property: if a temporal path condition for a path is satisfiable, then the ordinary boolean path condition for the path is satisfiable. The converse does not hold, indicating that temporal path conditions are more precise.

Download

  [PDF]   [DOI]

BibTeX

Authors at the institute

Department Head
Prof. Gregor Snelting
Former Staff Member
Dr. rer. nat. Andreas Lochbihler

Projects

Project
VALSOFT/Joana