Rail, Space, Security: Three Case Studies for SPARK 2014
Claire Dross, Pavlos Efstathopoulos, David Lesens, David Mentr, Yannick Moy · 2014
SPARK is a subset of the Ada programming language targeted at safety- and security-critical applications. SPARK 2014 is a ma- jor evolution of the SPARK language and toolset, that integrates formal program verication into ex- isting development processes, in order to decrease the cost of software verication, subject to cer- tication constraints. We present industrial case studies in three dierent certication domains that show the benets of using formal verication with SPARK 2014.