Inter-program Properties

DOI10.1007/978-3-642-03237-0_23MaRDI QIDQ3392934zbMATH OpenOpenAlexFDO

Authors Andrei Voronkov, Iman Narasamdya

Publication date 18 August 2009

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03237-0_23

zbMATH Keywords

assertion functioninvarianttranslation validation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Properties of concurrent programs
• Product programs and relational program logics
• Verification of Probabilistic Programs
• Proof-Producing Program Analysis
• scientific article; zbMATH DE number 4070286

Cites work

• An axiomatic basis for computer programming
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Certificate Translation for Optimizing Compilers
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Information flow inference for ML
• Inter-program Properties
• Is “sometime” sometimes better than “always”?
• Proving correctness of compiler optimizations by temporal logic
• Relational separation logic
• Simple relational correctness proofs for static analyses and program transformations
• Static Analysis
• Symbolic transfer function-based approaches to certified compilation

Cited in

(4)

• Product programs and relational program logics
• Relational decomposition
• Inter-program Properties
• Programming Languages and Systems

Describes a project that uses

Uses Software

• CoVaC

This page was built for publication: Inter-program Properties

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