Room 206 (2nd floor, badged access)
4 avril 2024 - 13h30
Abstract Interpreters: a Monadic Approach to Modular Verification
par Sébastien Michelland de LCIS (UGA)
Abstract: Abstract interpreters are a versatile type of static analyzers based on running programs in an “abstract domain” where termination is guaranteed. They're versatile because they have extensible components (like lattices and iteration strategies) that can be switched freely to derive varied analyses that are all sound based on meta-theoretical arguments. But they are not modular with respect to language features (memory scopes, side-effects, non-determinism, exceptions...) and this makes certification very monolithic—soundness proofs are usually tied to the denotation of a specific language, limiting reusability for a significant portion of the proof work.
Decoupling languages features is the purpose of layered monadic interpreters, which can be defined piecewise in a composable manner. The core idea is to keep subtle features as external calls at first, denote the program into a pure monad, and then implement the external calls step-by-step by enriching the program's environment with monad transformations. In this talk, I'll show that this process can also be used to define abstract interpreters and modularize their proofs, allowing certified components like “exceptional control flow” to be reused across languages. Better yet, it can be used to define concrete and abstract interpreters together, meaning many meta-theoretical arguments can be proven once-and-for-all, greatly reducing the proof effort for new interpreters.
(Joint work with Yannick ZAKOWSKI and Laure GONNORD. This talk will not assume prior knowledge of either abstract interpretation or monads.)
Presentation of the draft https://perso.ens-lyon.fr/yannick.zakowski/papers/itree-ai-draft.pdf
