Verified Characteristic Formulae for CakeML
| Autor: | Ramana Kumar, Michael Norrish, Armaël Guéneau, Magnus O. Myreen |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Soundness
Theoretical computer science Computer science Programming language 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Automated theorem proving 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Feature set computer Language semantics |
| Zdroj: | Programming Languages and Systems ISBN: 9783662544334 ESOP |
| DOI: | 10.1007/978-3-662-54434-1_22 |
| Popis: | 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 fully-fledged 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|