Paper Info
Title
Focused Certification of an Industrial Compilation and Static Verification Toolchain.
Abstract
SPARK 2014 is a subset of the Ada 2012 programming language that is supported by the GNAT compilation toolchain and multiple open source static analysis and verification tools. These tools can be used to verify that a SPARK 2014 program does not raise language-defined run-time exceptions and that it complies with formal specifications expressed as subprogram contracts. The results of analyses at source code level are valid for the final executable only if it can be shown that compilation/verification tools comply with a common deterministic programming language semantics.
Year
Venue
Field
2017
SEFM
Programming language,Spark (mathematics),Computer science,Source code,Static analysis,Real-time computing,Formal specification,Certification,Toolchain,Semantics,Executable
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
7
5
Name
Order
Citations
PageRank
Zhi Zhang1141.26
Robby21489104.82
John Hatcliff32373212.83
Yannick Moy4699.25
Pierre Courtieu516212.55