TY - GEN
T1 - Verified characteristic formulae for CakeML
AU - Guéneau, Armäel
AU - Myreen, Magnus O.
AU - Kumar, Ramana
AU - Norrish, Michael
N1 - Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.
PY - 2017
Y1 - 2017
N2 - 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 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.
AB - 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 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.
UR - http://www.scopus.com/inward/record.url?scp=85018690438&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-54434-1_22
DO - 10.1007/978-3-662-54434-1_22
M3 - Conference contribution
SN - 9783662544334
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 584
EP - 610
BT - Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
A2 - Yang, Hongseok
PB - Springer Verlag
T2 - 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Y2 - 22 April 2017 through 29 April 2017
ER -