Verifying B proof rules using deep embedding and automated theorem proving

DOI10.1007/978-3-642-24690-6_18MaRDI QIDQ3095242zbMATH OpenOpenAlexFDO

Authors Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois

Publication date 28 October 2011

Published in Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24690-6_18

zbMATH Keywords

verificationautomated theorem provingCoqproof rulesZenonB methoddeep embedding

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover
• Soundly proving B method formulæ using typed sequent calculus
• Why Would You Trust B?
• Verified Compilation and the B Method: A Proposal and a First Appraisal
• scientific article; zbMATH DE number 1746646

Cites work

• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• scientific article; zbMATH DE number 2079999 (Why is no real title available?)
• scientific article; zbMATH DE number 2080004 (Why is no real title available?)
• The B-Book
• Why Would You Trust B?
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

Cited in

(4)

• Guiding an automated theorem prover with neural rewriting
• Why Would You Trust B?
• Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover
• Soundly proving B method formulæ using typed sequent calculus

Describes a project that uses

Uses Software

• E Theorem Prover
• Atelier B
• Zenon
• Isabelle/HOL
• Coq

This page was built for publication: Verifying B proof rules using deep embedding and automated theorem proving

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