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.