Abstract Interpreters: a Monadic Approach to Modular Verification

This project contains the accompanying artifact to the CPP'24 submission "Abstract Interpreters: a Monadic Approach to Modular Verification".

We provide a library exposing reusable component for the simultaneous construction of monadic concrete and abstract interpreters, with a proof of soundness. We illustrate the use of the library on two illustrative examples: a structured, imperative, "Imp" language; and a assembly-like, control-flow-graph-based, "asm" language.

Meta

• Author(s):
  • [removed for double-blind evaluation]
• License: GPLv3
• Compatible Coq versions: >=8.17
• Additional dependencies:
  • dune
  • Extlib
  • InteractionTrees
  • Equations
• Coq namespace: ITreeAI

Structure

Internal library in theories/.

Definition of the aflow monad and the unfold function:

• AflowMonad.v Definition of the pairs of concrete/abstract control flow combinators:
• CombinatorSeq.v
• CombinatorIf.v
• CombinatorDo.v
• CombinatorWhile.v
• CombinatorCFG.v Definition of sound' and proof of sound_unfold:
• Interpretation.v

Case studies in theories/examples.

• Imp.v: Minimalist "Imp"
• ImpArith.v: Same language, treating arithmetic as an effect
• ImpArithFail.v: "Imp" with asserts, with three layers of interpretation
• Asm.v: Assembly-like language

Obtaining the project

git clone [removed for double-blind evaluation]
cd itree-ai

Building the project

Dependencies

Requires coq-ext-lib, coq-itree (dev version), equations and dune.

% opam install coq-ext-lib coq-itree.dev coq-equations dune

Building the project

dune build

Running the extracted abstract interpreters on a toy examples

% dune runtest

License

Some files related to base abstract domains are inspired from Xavier Leroy's IMP Abstract Interpreter (LPGL v2.1). The concrete semantics for the two example languages draw heavy inspiration from the tutorial for the Interaction Trees library (MIT). For now this code is licensed under GPLv3 (see LICENSE).