Extracting a data flow analyser in constructive logic

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

Authors Yanyan Li, David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu

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

• A formal executable semantics of the JavaCard platform
• Building certified static analysers by modular construction of well-founded lattices
• Development of an embedded verifier for Java card byte code using formal methods
• Formalizing a JVML verifier for initialization in a theorem prover
• Jakarta: A toolset for reasoning about JavaCard
• Operational semantics of the Java Card Virtual Machine
• Principles of program analysis
• 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)