Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq

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]

References

No references recorded for this publication.

Cited by

No citations of this publication recorded.