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

DOI10.1007/978-3-319-43144-4_20zbMATH Open1478.68048OpenAlexW2412986331MaRDI QIDQ2829268FDOQ2829268

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

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (3)

• Cogent: uniqueness types and certifying compilation
• Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code
• Computer Aided Verification

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)