A Certified Denotational Abstract Interpreter
From MaRDI portal
Publication:5747638
DOI10.1007/978-3-642-14052-5_3zbMath1291.68331OpenAlexW1847634121MaRDI 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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs ⋮ Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ Verified functional programming of an abstract interpreter ⋮ Constructive Galois Connections
Uses Software
This page was built for publication: A Certified Denotational Abstract Interpreter