Refinement through restraint: bringing down the cost of verification

DOI10.1145/2951913.2951940zbMath1361.68045OpenAlexW2430362266MaRDI QIDQ2982005

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

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

zbMATH Keywords

verificationprogramming languagessemanticsIsabelle/HOLfile systemslinear types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Verified Characteristic Formulae for CakeML ⋮ The verified CakeML compiler backend ⋮ A Framework for the Automatic Formal Verification of Refinement from Cogent to C ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code ⋮ Cogent: uniqueness types and certifying compilation ⋮ Flashix: modular verification of a concurrent and crash-safe flash file system

Uses Software

• Cogent
• Isabelle/HOL
• LLVM
• CakeML
• seL4
• go
• Pilsner
• Rust
• IOzone

This page was built for publication: Refinement through restraint: bringing down the cost of verification