A Machine Checked Soundness Proof for an Intermediate Verification Language

DOI10.1007/978-3-540-95891-8_51MaRDI QIDQ3599104zbMATH OpenOpenAlexFDO

Authors Frédéric Vogels, Bart Jacobs, Frank Piessens

Publication date 3 February 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://lirias.kuleuven.be/handle/123456789/222120

Mathematics Subject Classification ID

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

Recommendations

• A verified proof checker for higher-order logic
• scientific article; zbMATH DE number 1088222
• A Sound and Complete Deductive System for CTL* Verification
• Machine-checked proof-theory for propositional modal logics
• Machine Checking Proof Theory: An Application of Logic to Logic
• scientific article; zbMATH DE number 3907752
• scientific article; zbMATH DE number 7699423

Cites work

• A Machine Checked Soundness Proof for an Intermediate Verification Language
• A verifying compiler for a multi-threaded object-oriented language
• An axiomatic basis for computer programming
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Specification and verification challenges for sequential object-oriented programs

Cited in

(5)

• A polymorphic intermediate verification language: design and logical encoding
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• Verification Condition Generation Via Theorem Proving
• A generic intermediate representation for verification condition generation
• Towards a trustworthy semantics-based language framework via proof generation

Describes a project that uses

Uses Software

• KRAKATOA
• Caduceus
• Why3
• Spec#
• Boogie

This page was built for publication: A Machine Checked Soundness Proof for an Intermediate Verification Language

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