On Temporal Path Conditions in Dependence Graphs

12 years 26 days ago
On Temporal Path Conditions in Dependence Graphs
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 some 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, application of model checking to generate witnesses for a specific flow, and a case study. We prove the following soundness property: if a temporal path condition for a path is satisfiable, then the...
Andreas Lochbihler, Gregor Snelting
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where SCAM
Authors Andreas Lochbihler, Gregor Snelting
Comments (0)