Trustworthy Systems

CDSL version 1: Simplifying verification with linear types

Authors

Liam O'Connor, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah

NICTA

UNSW

Abstract

We introduce a purely functional domain specific language, CDSL, which aims to substantially reduce the cost of producing efficient, verified file system code. Given an executable specification of a file system, the CDSL compiler generates C code and, when fully implemented, will also generate an Isabelle/HOL proof linking the specification and the C implementation. We present two operational semantics for CDSL: (1) a value semantics, well suited for verification, and (2) an update semantics, which can be mapped to efficient C code. We outline the equivalence proof between these two semantics and discuss how the type system guarantees properties like termination, correct error handling, absence of memory leaks and aliasing.

BibTeX Entry

  @techreport{OConnorDavis_KAMKCR_14:tr,
    address          = {Sydney, Australia},
    author           = {O'Connor, Liam and Keller, Gabriele and Amani, Sidney and Murray, Toby and Klein, Gerwin and Chen,
                        Zilin and Rizkallah, Christine},
    institution      = {NICTA},
    issn             = {1833-9646-8393},
    month            = oct,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8393.pdf},
    title            = {{{CDSL}} Version 1: Simplifying Verification with Linear Types},
    year             = {2014}
  }

Download