Dependency analysis determines how entities (e.g. values of variables) computed in a program execution depend upon other entities (e.g. initial values of variables). Dependency appears in program safety (e.g. slicing) and security (e.g. privacy to prevent information leak). Dependency can only be defined by considering more than one trace (hence involves sets of sets of traces) which has been considered problematic for abstract interpretation (often considering trace properties i.e. set of traces). On the contrary, we show that the classical theory of abstract interpretation is directly applicable without needing any modification. We define the trace semantics of a while-language, its collecting semantics (strongest property), the dependency property, the dependency abstraction. and derive, by calculational design, a dependency analysis by abstract interpretation of the collecting semantics. By taking values into account, the analysis is more precise than classical, purely syntactic, analyzes.
Program Display Configuration
Sat 6 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Viennachange