Bibliographic Details
| Title: |
SPARK 2014 and GNATprove. |
| Authors: |
Hoang, Duc1 duc.hoang@epfl.ch, Moy, Yannick2 yannick.moy@adacore.com, Wallenburg, Angela3 angela.wallenburg@altran.com, Chapman, Roderick3 rod.chapman@altran.com |
| Source: |
International Journal on Software Tools for Technology Transfer. Nov2015, Vol. 17 Issue 6, p695-707. 13p. |
| Subjects: |
Software verification, SPARK (Computer program language), Compilers (Computer programs), Program development (Education), Computer architecture, Lexicography |
| Abstract: |
Extensive and expensive testing is the method most widely used for gaining confidence in safety-critical software. With a few exceptions, 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. (, ). 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. [ABSTRACT FROM AUTHOR] |
|
Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
