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.
(2019)
Ada Letters. ISSN 1094-3641
(Unpublished)
![[img]](https://oatao.univ-toulouse.fr/style/images/fileicons/application_pdf.png) |
(Document in English)
PDF (Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 508kB |
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 |
|---|---|
| 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
