CDSL Version 1: Simplifying Verification with Linear Types

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

Research output: Working paper

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.
Original languageEnglish
Place of PublicationSydney, Australia
PublisherNICTA
Number of pages22
ISBN (Print)1833-9646-8393
Publication statusPublished - 1 Oct 2014

Fingerprint

Dive into the research topics of 'CDSL Version 1: Simplifying Verification with Linear Types'. Together they form a unique fingerprint.

Cite this