{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:42Z","timestamp":1772164062378,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":11,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,11,10]],"date-time":"2013-11-10T00:00:00Z","timestamp":1384041600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,11,10]]},"DOI":"10.1145\/2527269.2527278","type":"proceedings-article","created":{"date-parts":[[2013,11,12]],"date-time":"2013-11-12T10:29:36Z","timestamp":1384252176000},"page":"21-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq"],"prefix":"10.1145","author":[{"given":"Pierre","family":"Courtieu","sequence":"first","affiliation":[{"name":"Conservatoire National des Arts et Metiers, Paris, France"}]},{"given":"Maria Virginia","family":"Aponte","sequence":"additional","affiliation":[{"name":"Conservatoire National des Arts et Metiers, Paris, France"}]},{"given":"Tristan","family":"Crolard","sequence":"additional","affiliation":[{"name":"Conservatoire National des Arts et Metiers, Paris, France"}]},{"given":"Zhi","family":"Zhang","sequence":"additional","affiliation":[{"name":"Kansas State University, Manhattan, KS, USA"}]},{"given":"Fnu","family":"Robby","sequence":"additional","affiliation":[{"name":"Kansas State University, manhattan, KS, USA"}]},{"given":"Jason","family":"Belt","sequence":"additional","affiliation":[{"name":"Kansas State University, Manhattan, USA"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[{"name":"Kansas State University, Manhattan, USA"}]},{"given":"Jerome","family":"Guitton","sequence":"additional","affiliation":[{"name":"AdaCore, Paris, France"}]},{"given":"Trevor","family":"Jennings","sequence":"additional","affiliation":[{"name":"Altran, Bath, England UK"}]}],"member":"320","published-online":{"date-parts":[[2013,11,10]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Ada reference manual. http:\/\/www.ada-auth.org\/standards\/ada12.html.  Ada reference manual. http:\/\/www.ada-auth.org\/standards\/ada12.html."},{"key":"e_1_3_2_1_2_1","unstructured":"Adacore Gnatprove tool. http:\/\/www.open-do.org\/projects\/hi-lite\/gnatprove\/.  Adacore Gnatprove tool. http:\/\/www.open-do.org\/projects\/hi-lite\/gnatprove\/."},{"key":"e_1_3_2_1_3_1","unstructured":"Adacore Hi-Lite project. http:\/\/www.open-do.org\/projects\/hi-lite\/.  Adacore Hi-Lite project. http:\/\/www.open-do.org\/projects\/hi-lite\/."},{"key":"e_1_3_2_1_4_1","unstructured":"Jago translation tool. https:\/\/github.com\/sireum\/bakar\/tree\/master\/sireum-bakarjago.  Jago translation tool. https:\/\/github.com\/sireum\/bakar\/tree\/master\/sireum-bakarjago."},{"key":"e_1_3_2_1_5_1","unstructured":"Sireum software analysis platform. http:\/\/www.sireum.org.  Sireum software analysis platform. http:\/\/www.sireum.org."},{"key":"e_1_3_2_1_6_1","volume-title":"SPARK 2014 language subset formalization. https:\/\/github.com\/sireum\/bakar\/tree\/master\/sireum-bakarformalization.","unstructured":"Source code for SPARK 2014 language subset formalization. https:\/\/github.com\/sireum\/bakar\/tree\/master\/sireum-bakarformalization. Source code for SPARK 2014 language subset formalization. https:\/\/github.com\/sireum\/bakar\/tree\/master\/sireum-bakarformalization."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_8_1","volume-title":"Oct","author":"Marsh W.","year":"1994","unstructured":"W. Marsh . Formal semantics of SPARK - static semantics , Oct 1994 . W. Marsh. Formal semantics of SPARK - static semantics, Oct 1994."},{"key":"e_1_3_2_1_9_1","volume-title":"Oct","author":"O'Neill I.","year":"1994","unstructured":"I. O'Neill . Formal semantics of SPARK - dynamic semantics , Oct 1994 . I. O'Neill. Formal semantics of SPARK - dynamic semantics, Oct 1994."},{"key":"e_1_3_2_1_10_1","volume-title":"Software considerations in airborne systems and equipment","author":"RTCA","year":"2011","unstructured":"RTCA DO-178. Software considerations in airborne systems and equipment , 2011 . RTCA DO-178. Software considerations in airborne systems and equipment, 2011."},{"key":"e_1_3_2_1_11_1","volume-title":"Formal methods supplement to do-178c and do-278a","author":"RTCA","year":"2011","unstructured":"RTCA DO-333. Formal methods supplement to do-178c and do-278a , 2011 . RTCA DO-333. Formal methods supplement to do-178c and do-278a, 2011."}],"event":{"name":"HILT 2013: High Integrity Language Technology ACM SIGAda Annual","location":"Pittsburgh Pennsylvania USA","acronym":"HILT 2013","sponsor":["Ada Europe Ada Europe","SIGAda ACM Special Interest Group on Ada Programming Language","SIGAPP ACM Special Interest Group on Applied Computing","SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems","SIGSOFT ACM Special Interest Group on Software Engineering","SIGCAS ACM Special Interest Group on Computers and Society","SIGCSE ACM Special Interest Group on Computer Science Education"]},"container-title":["Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2527269.2527278","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2527269.2527278","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:34:28Z","timestamp":1750217668000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2527269.2527278"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11,10]]},"references-count":11,"alternative-id":["10.1145\/2527269.2527278","10.1145\/2527269"],"URL":"https:\/\/doi.org\/10.1145\/2527269.2527278","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2658982.2527278","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,11,10]]},"assertion":[{"value":"2013-11-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}