| Static program analysis (s.p.a.) is utilized to reason about the run-time behavior of programs. Unfortunately, existing s.p.a. frameworks assume global (closed) programs, do not abstract well with regards to analysis or language, and lack a balance of compositionality with intensionality.;We formalize and implement a framework for modular, automated s.p.a. It analyzes individual modules, links their results and computes analysis of the linked modules. It abstracts over analysis and language. And, it combines syntax-directed flow with comprehensive flow maintenance.;We embark on natural semantics-based abstract interpretation as a generic s.p.a. framework that is both (semi)compositional and intensional. We obtain modularity through supercompilation (on-line partial evaluation) of natural semantics. First, we convert a classical natural semantics scheme into "small-step" tree-rewriting rules; these introduce "partial derivation trees" and enable supercompilation.;Secondly, we modify higher-order values (closures) into functions. This yields "higher-order" derivations, that embed closures that embed derivations, and enables computing upon and reasoning about program modules. For each conversion, we prove congruence of derivations of the transformed rules to those of the corresponding original rules. We adapt and apply supercompilation to the tree-rewriting "higher-order" semantics given a modular program to perform its static analysis; linking is specified as a substitution on partial derivations.;We validate feasibility of the project under two criteria: precision of analysis information and code improvement. Hence, we prescribe space-wise on-line optimizations for incremental construction of derivation trees interleaved with linking; the resulting link-time static analyzer computes the collecting semantics and the residual of a (partial) derivation tree. We then implement the optimized system, design comparative studies that test the different levels of each criterion, and conduct test cases on our system and two relevant existing systems.;These experiments reveal superiority of our system in both criteria and in other fundamental and pragmatic aspects. Importantly, they indicate a speed-up of analysis by modularity. The drawback is slow specialization (over data) that is correctable.;In summary, our system realizes a safe, sound and potentially competitive framework for modular s.p.a. This, with the formal specification, show feasibility of modular s.p.a. through partial evaluation. |
