SPARK 2014 and GNATprove.
Saved in:
| 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 |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 110204073 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: SPARK 2014 and GNATprove. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Hoang%2C+Duc%22">Hoang, Duc</searchLink><relatesTo>1</relatesTo><i> duc.hoang@epfl.ch</i><br /><searchLink fieldCode="AR" term="%22Moy%2C+Yannick%22">Moy, Yannick</searchLink><relatesTo>2</relatesTo><i> yannick.moy@adacore.com</i><br /><searchLink fieldCode="AR" term="%22Wallenburg%2C+Angela%22">Wallenburg, Angela</searchLink><relatesTo>3</relatesTo><i> angela.wallenburg@altran.com</i><br /><searchLink fieldCode="AR" term="%22Chapman%2C+Roderick%22">Chapman, Roderick</searchLink><relatesTo>3</relatesTo><i> rod.chapman@altran.com</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22International+Journal+on+Software+Tools+for+Technology+Transfer%22">International Journal on Software Tools for Technology Transfer</searchLink>. Nov2015, Vol. 17 Issue 6, p695-707. 13p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22SPARK+%28Computer+program+language%29%22">SPARK (Computer program language)</searchLink><br /><searchLink fieldCode="DE" term="%22Compilers+%28Computer+programs%29%22">Compilers (Computer programs)</searchLink><br /><searchLink fieldCode="DE" term="%22Program+development+%28Education%29%22">Program development (Education)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+architecture%22">Computer architecture</searchLink><br /><searchLink fieldCode="DE" term="%22Lexicography%22">Lexicography</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=110204073 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10009-014-0322-5 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 13 StartPage: 695 Subjects: – SubjectFull: Software verification Type: general – SubjectFull: SPARK (Computer program language) Type: general – SubjectFull: Compilers (Computer programs) Type: general – SubjectFull: Program development (Education) Type: general – SubjectFull: Computer architecture Type: general – SubjectFull: Lexicography Type: general Titles: – TitleFull: SPARK 2014 and GNATprove. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Hoang, Duc – PersonEntity: Name: NameFull: Moy, Yannick – PersonEntity: Name: NameFull: Wallenburg, Angela – PersonEntity: Name: NameFull: Chapman, Roderick IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 11 Text: Nov2015 Type: published Y: 2015 Identifiers: – Type: issn-print Value: 14332779 Numbering: – Type: volume Value: 17 – Type: issue Value: 6 Titles: – TitleFull: International Journal on Software Tools for Technology Transfer Type: main |
| ResultId | 1 |
