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

DOI10.1007/978-3-319-43144-4_20MaRDI QIDQ2829268zbMATH OpenOpenAlexFDO

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

(6)

• Cogent: uniqueness types and certifying compilation
• Computer Aided Verification
• Refinement through restraint: bringing down the cost of verification
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• Correctly compiling proofs about programs without proving compilers correct
• Formally verified suffix array construction

Describes a project that uses

Uses Software

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

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)