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 ordinary boolean path condition for the path is
satisfiable. The converse does not hold, indicating that temporal path conditions are more precise.
Keywords Program dependence graph - Path condition - Temporal logic - Security analysis
An extended abstract of the present article appeared in the 2007 Proceedings of the Seventh IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2007). The research of A. Lochbihler was partially supported by Deutsche Forschungsgemeinschaft, grant Sn11/9-1.