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]
@inproceedings{CourtieuACZRBHG13,
title = {Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq},
author = {Pierre Courtieu and Maria Virginia Aponte and Tristan Crolard and Zhi Zhang and Robby and Jason Belt and John Hatcliff and Jérôme Guitton and Trevor Jennings},
year = {2013},
doi = {10.1145/2527269.2527278},
url = {http://doi.acm.org/10.1145/2527269.2527278},
researchr = {https://researchr.org/publication/CourtieuACZRBHG13},
cites = {0},
citedby = {0},
pages = {21-22},
booktitle = {Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, HILT 2013, Pittsburgh, Pennsylvania, USA, November 10-14, 2013},
editor = {Jeff Boleng and S. Tucker Taft},
publisher = {ACM},
isbn = {978-1-4503-2467-0},
}