Verified Compilation and the B Method: A Proposal and a First Appraisal

DOI10.1016/J.ENTCS.2009.05.046MaRDI QIDQ5179355zbMATH OpenOpenAlexFDO

Authors Bartira Dantas, David Déharbe, Stephenson S. L. Galvão, Anamaria Martins Moreira, Valério Medeiros Júnior

Publication date 19 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.05.046

zbMATH Keywords

B methodverifying compiler

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 1956470
• Verification, Model Checking, and Abstract Interpretation
• The verified software repository: a step towards the verifying compiler
• scientific article; zbMATH DE number 1630130
• Verified bytecode verification and type-certifying compilation

Cites work

• Click'n prove: interactive proofs within set theory
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Refinement Calculus
• The B-Book
• Verification, Model Checking, and Abstract Interpretation

Cited in

(9)

• Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems
• B: Towards zero defect software
• Verifying B proof rules using deep embedding and automated theorem proving
• Relaxing Restrictions on Invariant Composition in the B Method by Ownership Control a la Spec#
• Why Would You Trust B?
• Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
• scientific article; zbMATH DE number 1258883 (Why is no real title available?)
• scientific article; zbMATH DE number 2079999 (Why is no real title available?)
• scientific article; zbMATH DE number 2090154 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle/HOL
• Coq
• Z

This page was built for publication: Verified Compilation and the B Method: A Proposal and a First Appraisal

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