Structural Abstract Interpretation: A Formal Study Using Coq
From MaRDI portal
Publication:5191090
DOI10.1007/978-3-642-03153-3_4zbMath1250.68089arXiv0810.2179OpenAlexW1784968340MaRDI QIDQ5191090
Publication date: 28 July 2009
Published in: Language Engineering and Rigorous Software Development (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0810.2179
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ View of Computer Algebra Data from Coq
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Proof-carrying code from certified abstract interpretation and fixpoint compression
- Programming Languages and Systems
- Formal certification of a compiler back-end or
- Building Certified Static Analysers by Modular Construction of Well-founded Lattices
- Theorem Proving in Higher Order Logics
- Types for Proofs and Programs
This page was built for publication: Structural Abstract Interpretation: A Formal Study Using Coq
