Formal proof of a program: find

DOI10.1016/J.SCICO.2006.10.002MaRDI QIDQ858911zbMATH OpenOpenAlexFDO

Authors Jean-Christophe Filliâtre

Publication date 11 January 2007

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2006.10.002

zbMATH Keywords

formal methodsHoare logicCoq proof assistantimperative programs

Mathematics Subject Classification ID

Theory of software (68N99) Abstract data types; algebraic specification (68Q65)

Recommendations

• The satisfiability of logical formula in proof of program
• scientific article; zbMATH DE number 4120164
• scientific article; zbMATH DE number 4006266
• Proofs as programs
• scientific article; zbMATH DE number 432701
• Writing programs that construct proofs
• Proofs and programs
• Proofs as efficient programs
• Proof-Producing Program Analysis
• scientific article; zbMATH DE number 962401

Cited in

(2)

• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Fifty years of Hoare's logic

Describes a project that uses

Uses Software

• Find
• Coq

This page was built for publication: Formal proof of a program: find

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