Bringing Effortless Refinement of Data Layouts to Cogent

Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, Gabriele Keller

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The language Cogent allows low-level operating system components to be modelled as pure mathematical functions operating on algebraic data types, which makes it highly suitable for verification in an interactive theorem prover. Furthermore, the Cogent compiler translates these models into imperative C programs, and provides a proof that this compilation is a refinement of the functional model. There remains a gap, however, between the C data structures used in the operating system, and the algebraic data types used by Cogent. This forces the programmer to write a large amount of boilerplate marshalling code to connect the two, which can lead to a significant runtime performance overhead due to excessive copying.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Modeling
Subtitle of host publication8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationCham
PublisherSpringer International Publishing
Pages134-149
Number of pages16
ISBN (Electronic)978-3-030-03418-4
ISBN (Print)978-3-030-03417-7
DOIs
Publication statusPublished - 29 Oct 2018
Event8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Limassol, Cyprus
Duration: 30 Oct 201813 Nov 2018
http://www.isola-conference.org/isola2018/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume11244
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation
Abbreviated titleISoLA 2018
Country/TerritoryCyprus
CityLimassol
Period30/10/1813/11/18
Internet address

Fingerprint

Dive into the research topics of 'Bringing Effortless Refinement of Data Layouts to Cogent'. Together they form a unique fingerprint.

Cite this