Paper Info
Title
Refinement through restraint: bringing down the cost of verification.
Abstract
We present a framework aimed at significantly reducing the cost of verifying certain classes of systems software, such as file systems. Our framework allows for equational reasoning about systems code written in our new language, Cogent. Cogent is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. Linear types allow us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. As Cogent is a restricted language, it is designed to easily interoperate with existing C functions and to connect to existing C verification frameworks. Our framework is based on certifying compilation: For a well-typed Cogent program, our compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.
Year
DOI
Venue
2016
10.1145/2951913.2951940
ICFP
Field
DocType
Citations 
HOL,Programming language,Computer science,Interoperability,Compiler,Theoretical computer science,Code generation,Mathematical proof,Software,Garbage collection,Semantics
Conference
8
PageRank 
References 
Authors
0.55
28
9
Name
Order
Citations
PageRank
Liam O'Connor1445.02
Zilin Chen2232.53
Christine Rizkallah37514.05
Sidney Amani4675.00
Japheth Lim5402.95
Toby Murray624217.03
Yutaka Nagashima7236.13
Thomas Sewell891437.60
Gerwin Klein9145087.47