Extracting a data flow analyser in constructive logic

DOI10.1016/J.TCS.2005.06.004MaRDI QIDQ2566027zbMATH OpenOpenAlexFDO

Authors 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

constraint-based data flow analysisCoq proof assistant

Mathematics Subject Classification ID

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

Recommendations

• Programming Languages and Systems
• Building certified static analysers by modular construction of well-founded lattices
• Certified Static Analysis by Abstract Interpretation
• Types for Proofs and Programs
• A certified denotational abstract interpreter

Cites work

• Building certified static analysers by modular construction of well-founded lattices
• scientific article; zbMATH DE number 1692947 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1796120 (Why is no real title available?)
• scientific article; zbMATH DE number 1848374 (Why is no real title available?)
• scientific article; zbMATH DE number 2090143 (Why is no real title available?)
• Operational semantics of the Java Card Virtual Machine
• Programming Languages and Systems
• Verified bytecode verifiers.

Cited in

(10)

• Generating data flow analysis algorithms from modal specifications
• A formally verified compiler back-end
• 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
• Modular development of certified program verifiers with a proof assistant,
• Verifying a local generic solver in Coq
• Programming Languages and Systems
• Building certified static analysers by modular construction of well-founded lattices
• Control-flow analysis of function calls and returns by abstract interpretation

Describes a project that uses

Uses Software

• Coq
• Jakarta
• OCaml

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2566027)