Paper Info
Title
Spark 2014 And Gnatprove A Competition Report From Builders Of An Industrial-Strength Verifying Compiler
Abstract
Extensive and expensive testing is the method most widely used for gaining confidence in safety-critical software. With a fewexceptions, such as SPARK, formal verification is rarely used in industry due to its high cost and level of skill required. The grand challenge of building a verifying compiler for static formal verification of programs aims at bringing formal verification to non-expert users of powerful programming languages. This challenge has nurtured competition and collaboration among verification tool builders; an example is the VerifyThis competition Huisman et al. (http://digbib.ubka.uni-karlsruhe.de/volltexte/1000034373, 2013). In this paper, we describe our approach to popularising formal verification in the design of the SPARK 2014 language and the associated formal verification tool GNATprove. In particular, we present our solution to combining tests and proofs, which provides a cost-competitive way to develop software to standards such as do-178. At the heart of our technique are executable contracts, and the ability to both test and prove those. We use running examples from the VerifyThis 2012 competition and discuss the results of using our tools on those problems.
Year
DOI
Venue
2015
10.1007/s10009-014-0322-5
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
Keywords
DocType
Volume
SPARK, Ada, Program verification, Verifying compiler, Deductive verification, Static analysis
Journal
17
Issue
ISSN
Citations 
6
1433-2779
0
PageRank 
References 
Authors
0.34
7
4
Name
Order
Citations
PageRank
Duc L. N. Hoang1215.76
Yannick Moy2699.25
Angela Wallenburg3263.46
Rod Chapman4928.44