CDSL Version 1: Simplifying Verification with Linear Types

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

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 language	English
Place of Publication	Sydney, Australia
Publisher	NICTA
Number of pages	22
ISBN (Print)	1833-9646-8393
Publication status	Published - 1 Oct 2014

Access to Document

https://ts.data61.csiro.au/publications/nicta_full_text/8393.pdfLicence: All Rights Reserved

Cite this

@techreport{548da7209642409dbdeb62392a1c8ecb,

title = "CDSL Version 1: Simplifying Verification with Linear Types",

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.",

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

year = "2014",

month = oct,

day = "1",

language = "English",

isbn = "1833-9646-8393",

publisher = "NICTA",

type = "WorkingPaper",

institution = "NICTA",

}

TY - UNPB

T1 - CDSL Version 1: Simplifying Verification with Linear Types

AU - O'Connor-Davis, Liam

AU - Keller, Gabriele

AU - Amani, Sidney

AU - Murray, Toby

AU - Klein, Gerwin

AU - Chen, Zilin

AU - Rizkallah, Christine

PY - 2014/10/1

Y1 - 2014/10/1

N2 - 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.

AB - 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.

M3 - Working paper

SN - 1833-9646-8393

BT - CDSL Version 1: Simplifying Verification with Linear Types

PB - NICTA

CY - Sydney, Australia

ER -

CDSL Version 1: Simplifying Verification with Linear Types

Abstract

Access to Document

Fingerprint

Cite this