Formal proof of a program: find

DOI10.1016/J.SCICO.2006.10.002zbMATH Open1178.68353OpenAlexW1971879297MaRDI QIDQ858911FDOQ858911

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

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

zbMATH Keywords

formal methodsHoare logicCoq proof assistantimperative programs

Mathematics Subject Classification ID

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

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

Uses Software

• Coq
• Find

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)