OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Teaching formal methods through Frama-C & SPARK

Garion, Christophe and Hugues, Jérôme Teaching formal methods through Frama-C & SPARK. (2019) In: Frama-C & SPARK Day 2019, 3 June 2019 - 3 June 2019 (Paris, France). (Unpublished)

(Document in English)

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


How can we educate future engineers about formal methods in few hours when they do not have a strong background in theoretical Computer Science? That is a challenge we are trying to take up at ISAE-SUPAERO in the critical systems architecture curriculum. We will present some feedback on what the students can learn and do in less than 15 hours and also present SPARK by Example, an adaptation of ACSL by Example mainly developed by two undergraduates in less than 3 months.

Item Type:Other Conference
Audience (conference):International conference without published proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Laboratory name:
Deposited On:31 Jul 2019 07:06

Repository Staff Only: item control page