Pierre Courtieu, Maria Virginia Aponte, Tristan Crolard, Zhi Zhang, Robby, Jason Belt, John Hatcliff, Jérôme Guitton, Trevor Jennings. Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. In Jeff Boleng, S. Tucker Taft, editors, Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, HILT 2013, Pittsburgh, Pennsylvania, USA, November 10-14, 2013. pages 21-22, ACM, 2013. [doi]
Abstract is missing.