A Certified Denotational Abstract Interpreter
From MaRDI portal
Publication:5747638
DOI10.1007/978-3-642-14052-5_3zbMath1291.68331MaRDI QIDQ5747638
David Cachera, David Pichardie
Publication date: 14 September 2010
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00537810/file/main.pdf
Related Items
Constructive Galois Connections, Verified abstract interpretation techniques for disassembling low-level self-modifying code, Verified functional programming of an abstract interpreter, Automatically proving termination and memory safety for programs with pointer arithmetic, Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
Uses Software