The spirit of ghost code
From MaRDI portal
Publication:518394
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
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
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