Verified characteristic formulae for CakeML
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]
|Collections||ANU Research Publications|
|Source:||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.