Compositional Soundness Proofs of Abstract Interpreters

Sven Keidel

Date: Wed, May 02, 2018
Time: 12:00

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 |
Next: |