Why Would You Trust B?

DOI10.1007/978-3-540-75560-9_22MaRDI QIDQ3498474zbMATH OpenOpenAlexFDO

Authors Éric Jaeger, Catherine Dubois

Publication date 15 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75560-9_22

zbMATH Keywords

ConfidenceDeep embeddingFormal MethodsProver

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 1615249
• scientific article; zbMATH DE number 2172802
• Verifying B proof rules using deep embedding and automated theorem proving
• Verified Compilation and the B Method: A Proposal and a First Appraisal
• Soundly proving B method formulæ using typed sequent calculus

Cites work

• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• scientific article; zbMATH DE number 2090073 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Confluence properties of weak and strong calculi of explicit substitutions
• Engineering formal metatheory
• Explicit substitutions
• The B-Book
• Theorem Proving in Higher Order Logics
• de Bruijn notation as a nested datatype

Cited in

(4)

• scientific article; zbMATH DE number 2172802 (Why is no real title available?)
• scientific article; zbMATH DE number 1615249 (Why is no real title available?)
• Soundly proving B method formulæ using typed sequent calculus
• Verifying B proof rules using deep embedding and automated theorem proving

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Why Would You Trust B?

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