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

DOI10.1016/j.entcs.2009.05.046zbMath1347.68079OpenAlexW1982085713MaRDI QIDQ5179355

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

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)

Uses Software

• Coq
• Isabelle/HOL
• Z

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• Click’n Prove: Interactive Proofs within Set Theory
• The B-Book
• Refinement Calculus
• Formal certification of a compiler back-end or
• Verification, Model Checking, and Abstract Interpretation

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