Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving

DOI10.1007/978-3-642-24690-6_18zbMath1350.68236OpenAlexW2213028572MaRDI QIDQ3095242

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

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

verificationB methodautomated theorem provingCoqproof rulesZenondeep embedding

Mathematics Subject Classification ID

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

Related Items (1)

Soundly Proving B Method Formulæ Using Typed Sequent Calculus

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Why Would You Trust B?
• The B-Book

This page was built for publication: Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving