Formalization of a SPARK Subset in Coq

by Yannick Moy in Language, Formal Verification, Events, Papers and Slides – December 6, 2013

Currently, only a small part of SPARK 2014 has been formalized, but the architecture put in place already allows reading the abstract syntax tree produced by the GNAT compiler frontend and checking that the equivalent generated abstract syntax tree in Coq is well-formed and has the desired run-time checks. See the attached slides of the presentation that Zhi gave at HILT conference last month.


comments powered by Disqus