OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists

Creuse, Léo and Dross, Claire and Garion, Christophe and Hugues, Jérôme and Huguet, Joffrey Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists. (2019) In: 3rd World Congress on Formal Methods, 7 November 2019 - 11 November 2019 (Porto, Portugal).

[img] (Document in English)

PDF (Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/978-3-030-32441-4_2


Deductive verification of software is a formal method that is usually taught in Computer Science curriculum. But how can students with no strong background in Computer Science be exposed to such a technique? We present in this paper two experiments made at ISAE-SUPAERO, an engineering program focusing on aerospace industry. The first one is a classic lecture introducing deductive methods through the Frama-C platform or the SPARK programming language. The second one is the production by two undergraduate students of a complete guide on how to prove complex algorithms with SPARK. Both experiments showed that students with no previous knowledge of formal methods nor theoretical Computer Science may learn deductive methods efficiently with bottom-up approaches in which they are quickly confronted to tools and practical sessions.

Item Type:Conference or Workshop Item (Paper)
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Other partners > AdaCore (FRANCE)
Laboratory name:
Deposited On:06 Dec 2019 15:19

Repository Staff Only: item control page