Why Would You Trust B?

DOI10.1007/978-3-540-75560-9_22zbMATH Open1137.68355OpenAlexW1479826380MaRDI QIDQ3498474FDOQ3498474

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

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

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)

Cites Work

• The B-Book
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• Title not available (Why is that?)
• Engineering formal metatheory
• Explicit substitutions
• de Bruijn notation as a nested datatype
• Title not available (Why is that?)
• Confluence properties of weak and strong calculi of explicit substitutions

Cited In (4)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Soundly proving B method formulæ using typed sequent calculus
• Verifying B proof rules using deep embedding and automated theorem proving

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)