|
 
|
[CZR17] Focused Certification of an Industrial Compilation and Static Verification Toolchain
Conférence Internationale avec comité de lecture : Software Engineering and Formal Methods (SEFM), August 2017, Vol. 10469, pp.17-34, Series LNCS, Trento, Italy, (DOI: 10.1007/978-3-319-66197-1_2)Mots clés: Semantics, programming languages, verification, formal methods
Résumé:
In this paper, we present: (a) a mechanized formal semantics for a large subset of SPARK 2014, (b) an architecture for creating certified/certifying analysis and verification tools for SPARK, and (c) tools and mechanized proofs that instantiate that architecture to demonstrate that SPARK-relevant Ada run-time checks inserted by the GNAT compiler are correct; this includes mechanized proofs of correctness for abstract interpretation-based static analyses that are used to certify correctness of GNAT run-time check optimizations.
Collaboration:
CIS@K-STATE
BibTeX
| @inproceedings { | |||
| CZR17, | |||
| title | = | "{Focused Certification of an Industrial Compilation and Static Verification Toolchain}", | |
| author | = | " P. Courtieu and Z. Zhang and Robby and J. Hatcliff and Y. Moy ", | |
| booktitle | = | "{Software Engineering and Formal Methods (SEFM)}", | |
| year | = | 2017, | |
| month | = | "August", | |
| series | = | "LNCS", | |
| volume | = | 10469, | |
| pages | = | "17-34", | |
| address | = | "Trento, Italy", | |
| doi | = | "10.1007/978-3-319-66197-1_2", | |
| } | |||
