Compositional Soundness Proofs of Abstract Interpreters

Sven Keidel

There are two kinds of static analyses for imperative programming languages such as the While-language - Value analyses that analyze values of the language, e.g., what range of numbers a numeric variable can hold, and effect analyses that analyze the effect of destructive updates, e.g., which variable definitions are reachable and have not been overridden.

In this talk I present how value and effect analyses can be defined and seamlessly be combined with arrow transformers. This modular definition of the analyses also gives rise to compositional soundness proofs - Only one soundness proof per value analyses and effect analyses is required. In particular, soundness of a combined analysis follows for free by composing the proofs of value and effect analysis.

---

Previous: Tim Rensen | The Design and Implementation of a Domain-Specific Language for the Description of Medical Devices
Next: | Portable Editor Services