OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

SPARK by Example: an introduction to formal verification through the standard C++ library

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

[img]
Preview
(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 On:07 Mar 2019 09:04

Repository Staff Only: item control page