Paper Info
Title
Tutorial: A Practical Introduction to Formal Development and Verification of High-Assurance Software with SPARK
Abstract
Summary form only given, as follows. The complete presentation was not made available for publication as part of the conference proceedings. This hands-on tutorial will show attendees how to use formal methods in developing and verifying high-assurance software. It will cover the benefits and costs of formal methods technology, describe its capabilities and limits, summarize how to adopt formal methods at varying levels depending on assurance requirements, show how to combine formal methods with traditional testing-based techniques, and highlight industrial experience. The SPARK language (a subset of Ada 2012) will be used as the vehicle for explaining formal methods. The techniques presented can be applied to other language technologies, and the tutorial will compare the SPARK and Frama-C approaches. Demonstrations will use the GNATprove toolset, and hands-on exercises will be drawn from the SPARK section of the learn.adacore.com site.
Year
DOI
Venue
2019
10.1109/SecDev.2019.00012
2019 IEEE Cybersecurity Development (SecDev)
Keywords
Field
DocType
formal methods, high-assurance software, safety critical software, high-security software, software verification, SPARK language
Spark (mathematics),Software engineering,Computer science,Formal development,Software,High assurance,Formal methods,Software verification
Conference
ISBN
Citations 
PageRank 
978-1-5386-7290-7
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Benjamin M. Brosgol100.34
Claire Dross2214.52
Yannick Moy3699.25