Creuse, Léo
and Huguet, Joffrey and Garion, Christophe and Hugues, Jérôme
SPARK by Example: an introduction to formal verification through the standard C++ library.
(2018)
Ada Letters, 38 (2). 89-96. ISSN 1094-3641
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 558kB |
Official URL: https://doi.org/10.1145/3375408.3375415
Abstract
This paper presents SPARK by Example, a guide for people wanting to get involved in formal verification of SPARK programs. SPARK by Example is inspired by ACSL by Example, a similar effort for C/ACSL programs, and provides detailed specification, implementation and proof of classic algorithms (array manipulation, sorting, heap etc). A comparison between ACSL and SPARK is done in the light of proof performance and ease of use.
| Item Type: | Article |
|---|---|
| HAL Id: | hal-02417184 |
| Audience (journal): | International peer-reviewed journal |
| Uncontrolled Keywords: | |
| Institution: | Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE) |
| Laboratory name: | |
| Statistics: | download |
| Deposited By: | Christophe Garion |
| Deposited On: | 07 Mar 2019 09:04 |
Repository Staff Only: item control page
