Refinement through restraint: bringing down the cost of verification
DOI10.1145/2951913.2951940zbMATH Open1361.68045OpenAlexW2430362266WikidataQ130970044 ScholiaQ130970044MaRDI QIDQ2982005FDOQ2982005
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
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
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)
Cited In (6)
- Cogent: uniqueness types and certifying compilation
- Flashix: modular verification of a concurrent and crash-safe flash file system
- Verified characteristic formulae for CakeML
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- Ready, set, verify! Applying hs-to-coq to real-world Haskell code
- The verified CakeML compiler backend
Uses Software
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)
