A framework for the automatic formal verification of refinement from \textsc{Cogent} to C

DOI10.1007/978-3-319-43144-4_20MaRDI QIDQ2829268zbMATHOpenAlexFDO

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

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-43144-4_20

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Refinement through restraint: bringing down the cost of verification
• scientific article; zbMATH DE number 2090154
• Computer Aided Verification
• Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
• Cogent: uniqueness types and certifying compilation

Cites work

• CakeML
• Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Refinement through restraint: bringing down the cost of verification
• Secure Microkernels, State Monads and Scalable Refinement
• Types, bytes, and separation logic

Cited in

(4)

• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• Refinement through restraint: bringing down the cost of verification
• Cogent: uniqueness types and certifying compilation
• Computer Aided Verification

Describes a project that uses

Uses Software

• Isabelle/HOL
• CakeML
• seL4
• Cogent
• GitHub

This page was built for publication: A framework for the automatic formal verification of refinement from \textsc{Cogent} to C

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