A Framework for the Automatic Formal Verification of Refinement from Cogent to C

DOI10.1007/978-3-319-43144-4_20zbMath1478.68048OpenAlexW2412986331MaRDI QIDQ2829268

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

Mathematics Subject Classification ID

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

Related Items (2)

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

Uses Software

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

Cites Work

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

This page was built for publication: A Framework for the Automatic Formal Verification of Refinement from Cogent to C