CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Verified characteristic formulae for CakeML

A. Guéneau ; Magnus O. Myreen (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)) ; R. Kumar ; M. Norrish
Lecture Notes in Computer Science - 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, 22-29 April 2017 (0302-9743). Vol. 10201 (2017), p. 584-610.
[Konferensbidrag, refereegranskat]

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.



Denna post skapades 2017-05-31. Senast ändrad 2017-06-28.
CPL Pubid: 249541

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)

Ämnesområden

Datavetenskap (datalogi)

Chalmers infrastruktur