Skip to main content

TS

CDSL version 1: Simplifying verification with linear types

Authors

Liam O'Connor-Davis, 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,
    author           = {O'Connor-Davis, Liam and Keller, Gabriele and Amani, Sidney and Murray, Toby and Klein, Gerwin and
                        Chen, Zilin and Rizkallah, Christine},
    issn             = {1833-9646-8393},
    year             = {2014},
    month            = {oct},
    address          = {Sydney, Australia},
    title            = {{{CDSL}} Version 1: Simplifying Verification with Linear Types},
    type             = {Technical Report},
    institution      = {NICTA}
  }

Download