Skip navigation
Skip navigation

Verified characteristic formulae for CakeML

Guéneau, Armäel; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael

Description

Characteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a programming language (OCaml). This leaves a gap between what is established by the verification framework and the program that actually runs. We present a fullyfledged CF framework for the formally specified CakeML programming language. Our framework...[Show more]

dc.contributor.authorGuéneau, Armäel
dc.contributor.authorMyreen, Magnus O.
dc.contributor.authorKumar, Ramana
dc.contributor.authorNorrish, Michael
dc.contributor.editorYang, H.
dc.coverage.spatialUppsala, Sweden
dc.date.accessioned2020-12-20T20:58:28Z
dc.date.available2020-12-20T20:58:28Z
dc.date.createdApril 22-29 2017
dc.identifier.isbn9783662544334
dc.identifier.urihttp://hdl.handle.net/1885/218599
dc.description.abstractCharacteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a programming language (OCaml). This leaves a gap between what is established by the verification framework and the program that actually runs. We present a fullyfledged CF framework for the formally specified CakeML programming language. Our framework extends the existing CF approach to support exceptions and I/O, thereby covering the full feature set of CakeML, and comes with a formally verified soundness theorem. Furthermore, it integrates with existing proof techniques for verifying CakeML programs. This validates the CF approach, and allows users to prove end-to-end theorems for higher-order imperative programs, from specification to language semantics, within a single theorem prover
dc.format.mimetypeapplication/pdf
dc.language.isoen_AU
dc.publisherSpringer
dc.relation.ispartofseries26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
dc.sourceLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.titleVerified characteristic formulae for CakeML
dc.typeConference paper
local.description.notesImported from ARIES
local.description.refereedYes
dc.date.issued2017
local.identifier.absfor080308 - Programming Languages
local.identifier.ariespublicationa383154xPUB5907
local.type.statusMetadata only
local.contributor.affiliationGuéneau, Armäel, École Normale Supérieure
local.contributor.affiliationMyreen, Magnus O., University of Cambridge
local.contributor.affiliationKumar, Ramana, CSIRO/UNSW
local.contributor.affiliationNorrish, Michael, College of Engineering and Computer Science, ANU
local.bibliographicCitation.startpage584
local.bibliographicCitation.lastpage610
local.identifier.doi10.1007/978-3-662-54434-1_22
dc.date.updated2020-11-23T11:26:24Z
local.identifier.scopusID2-s2.0-85018690438
CollectionsANU Research Publications

Download

There are no files associated with this item.


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator