Refinement through restraint: bringing down the cost of verification

DOI10.1145/2951913.2951940MaRDI QIDQ2982005zbMATH OpenOpenAlexWikidataFDO

Authors Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas D. Sewell, Gerwin Klein

Publication date 10 May 2017

Published in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2951913.2951940

zbMATH Keywords

file systemsIsabelle/HOLlinear typesprogramming languagessemanticsverification

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• Cogent: uniqueness types and certifying compilation
• Effective interactive proofs for higher-order imperative programs
• Computer Aided Verification
• Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction

Cited in

(7)

• Flashix: modular verification of a concurrent and crash-safe flash file system
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• Verified characteristic formulae for CakeML
• The verified CakeML compiler backend
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• Cogent: uniqueness types and certifying compilation
• Formally verified suffix array construction

Describes a project that uses

Uses Software

• Cogent
• Isabelle/HOL
• IOzone
• LLVM
• CakeML
• seL4
• Pilsner
• go
• Rust

This page was built for publication: Refinement through restraint: bringing down the cost of verification

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