The spirit of ghost code

DOI10.1007/s10703-016-0243-xzbMath1358.68070OpenAlexW2318327664MaRDI QIDQ518394

Léon Gondelman, Andrei Paskevich, Jean-Christophe Filliâtre

Publication date: 28 March 2017

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-016-0243-x

zbMATH Keywords

deductive software verificationghost codeWhy3

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 (4)

WhyMP, a formally verified arbitrary-precision integer library ⋮ An automated deductive verification framework for circuit-building quantum programs ⋮ The spirit of ghost code ⋮ Unnamed Item

Uses Software

• Dafny
• Why3
• VCC
• WhyML

Cites Work

• Unnamed Item
• Unnamed Item
• The spirit of ghost code
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A syntactic approach to type soundness
• Hoare logic and auxiliary variables
• Behavioral interface specification languages
• A Structural Approach to Prophecy Variables
• Information flow inference for free
• Dafny: An Automatic Program Verifier for Functional Correctness
• Certification of programs for secure information flow
• Information flow inference for ML
• Why3 — Where Programs Meet Provers

This page was built for publication: The spirit of ghost code