A proof method for the correctness of modularized 0CFA

摘要

Modular program analysis, which analyzes sepa- rated program sources such as modules, is a practical alternative to whole-program analysis. It does not need the entire program text as its input,and if some parts of the program are modified, it re-analyzes only the dependent parts of a modified module. This article is about our findings when we tried To derive a modular version from a whole-program Control-flow analysis (CFA) [1-3], to be used inside a Modulrized version of our exception analysis [4-6]: ·Deriving a modular version from a whole-program monovariant (or context-insensitive) CFA makes the resulting analysis polyvariant (or context- sensitive) at the module level. ·Hence the correctness of its modularized version cannot be proven in general with respect to the original CFA. ·A convenient stepping stone to prove the correct ness of a modularized version(instead of proving it against the program semantics) is a whole-program CFA that is polyvariant at the module level.