Building Certified Static Analysers by Modular Construction of Well-founded Lattices

DOI10.1016/j.entcs.2008.04.064zbMath1286.68401OpenAlexW1976691484MaRDI QIDQ5415621

David Pichardie

Publication date: 13 May 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.04.064

zbMATH Keywords

static analysisproof assistantconstructive proofs

Mathematics Subject Classification ID

Related Items (4)

Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ Certified Static Analysis by Abstract Interpretation ⋮ Structural Abstract Interpretation: A Formal Study Using Coq ⋮ Extracting a data flow analyser in constructive logic

Uses Software

• Coq
• OCaml
• ASTREE

Cites Work

• Unnamed Item
• The octagon abstract domain
• Constructing recursion operators in intuitionistic type theory
• Verified bytecode verifiers.
• Extracting a data flow analyser in constructive logic
• Systematic design of program transformation frameworks by abstract interpretation
• Programming Languages and Systems
• Programming Languages and Systems
• Formal certification of a compiler back-end or
• Fundamental Approaches to Software Engineering
• Types for Proofs and Programs
• Types for Proofs and Programs

This page was built for publication: Building Certified Static Analysers by Modular Construction of Well-founded Lattices