Extracting a data flow analyser in constructive logic

DOI10.1016/j.tcs.2005.06.004zbMath1077.68051OpenAlexW2009375997MaRDI QIDQ2566027

Yanyan Li

Publication date: 22 September 2005

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.06.004

zbMATH Keywords

Coq proof assistantconstraint-based data flow analysis

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ A Certified Data Race Analysis for a Java-like Language ⋮ Certified Static Analysis by Abstract Interpretation ⋮ A formally verified compiler back-end ⋮ Control-flow analysis of function calls and returns by abstract interpretation ⋮ Modular development of certified program verifiers with a proof assistant, ⋮ Building Certified Static Analysers by Modular Construction of Well-founded Lattices

Uses Software

• Coq
• Jakarta
• OCaml

Cites Work

• Verified bytecode verifiers.
• Operational semantics of the Java Card Virtual Machine
• Programming Languages and Systems
• Building Certified Static Analysers by Modular Construction of Well-founded Lattices
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Extracting a data flow analyser in constructive logic