Weakest precondition for general recursive programs formalized in Coq

DOI10.1007/3-540-45685-6_22MaRDI QIDQ4484349zbMATH OpenFDO

Authors M. Munro, Lin Hu, Mark Harman, Xingyuan Zhang

Publication date 12 June 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2410/24100332.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Weakest Preconditions for High-Level Programs
• scientific article; zbMATH DE number 1531358
• Safety and progress of recursive procedures
• scientific article; zbMATH DE number 3974258
• scientific article; zbMATH DE number 4047056

Cited in

(9)

• Instrumenting a weakest precondition calculus for counterexample generation
• Weakest pre-condition reasoning for Java programs with JML annotations
• Combining dynamic and static slicing for analysing assembler
• Weakest preconditioned goto axiom
• Verifying and generating WP transformers for procedures on complex data
• Representing WP semantics in Isabelle/ZF
• Formalization of Refinement Calculus for Reactive Systems
• Algebra of Monotonic Boolean Transformers
• Provably correct derivation of algorithms using FermaT

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Weakest precondition for general recursive programs formalized in Coq

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