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. (2019) Ada Letters. ISSN 1094-3641 (Unpublished)

[img] (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