A Machine Checked Soundness Proof for an Intermediate Verification Language

DOI10.1007/978-3-540-95891-8_51zbMath1206.68193OpenAlexW1510623049MaRDI QIDQ3599104

Bart Jacobs, Frédéric Vogels, 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

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

Related Items (1)

A Machine Checked Soundness Proof for an Intermediate Verification Language

Uses Software

• KRAKATOA
• Why3
• Spec#
• Caduceus
• Boogie

Cites Work

• 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
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• An axiomatic basis for computer programming
• Unnamed Item

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