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

verificationprogramming languagessemanticsIsabelle/HOLfile systemslinear types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) 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

(6)

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

Describes a project that uses

Uses Software

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

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)