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]

CollectionsANU Research Publications
Date published: 2017
Type: Conference paper
URI: http://hdl.handle.net/1885/218599
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI: 10.1007/978-3-662-54434-1_22

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