{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:37Z","timestamp":1772164057479,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,10,18]],"date-time":"2014-10-18T00:00:00Z","timestamp":1413590400000},"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":[[2014,10,18]]},"DOI":"10.1145\/2663171.2663179","type":"proceedings-article","created":{"date-parts":[[2014,10,14]],"date-time":"2014-10-14T08:29:24Z","timestamp":1413275364000},"page":"5-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Can C++ be made as safe as SPARK?"],"prefix":"10.1145","author":[{"given":"David","family":"Crocker","sequence":"first","affiliation":[{"name":"Escher Technologies Ltd., Aldershot, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2014,10,18]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"957290","article-title":"SPARK - The Proven Approach to High Integrity Software","volume":"978","author":"Barnes John","year":"2012","unstructured":"Barnes , John . \" SPARK - The Proven Approach to High Integrity Software \". ISBN 978-0 - 957290 - 957250 -1, 2012 . Barnes, John. \"SPARK - The Proven Approach to High Integrity Software\". ISBN 978-0-957290-50-1, 2012.","journal-title":"ISBN"},{"key":"e_1_3_2_1_2_1","first-page":"906400","article-title":"Guidelines for the Use of the C Language in Critical Systems","volume":"978","unstructured":"MIRA . \" Guidelines for the Use of the C Language in Critical Systems \", ISBN 978-1 - 906400 - 906410 -1 (paperback), ISBN 978-1-906400-11-8 (PDF), 2013. MIRA . \"Guidelines for the Use of the C Language in Critical Systems\", ISBN 978-1-906400-10-1 (paperback), ISBN 978-1-906400-11-8 (PDF), 2013.","journal-title":"ISBN"},{"key":"e_1_3_2_1_3_1","first-page":"03","article-title":"Guidelines for the Use of the C++ Language in Critical Systems","volume":"978","author":"MIRA.","unstructured":"MIRA. \" Guidelines for the Use of the C++ Language in Critical Systems \", ISBN 978-906400 - 03 - 03 (paperback), ISBN 978-906400-04-0 (PDF), 2008. MIRA. \"Guidelines for the Use of the C++ Language in Critical Systems\", ISBN 978-906400-03-3 (paperback), ISBN 978-906400-04-0 (PDF), 2008.","journal-title":"ISBN"},{"key":"e_1_3_2_1_4_1","volume-title":"December","author":"Lockheed Martin Joint Strike","year":"2005","unstructured":"Lockheed Martin . \" Joint Strike Fighter Air Vehicle C++ Coding Standards for the System Development and Demonstration Program\" , Document Number 2RDU00001 Rev C , December 2005 . Lockheed Martin. \"Joint Strike Fighter Air Vehicle C++ Coding Standards for the System Development and Demonstration Program\", Document Number 2RDU00001 Rev C, December 2005."},{"key":"e_1_3_2_1_5_1","unstructured":"ISO\/IEC 14882:2003 \"Programming languages - C++\" 2003.  ISO\/IEC 14882:2003 \"Programming languages - C++\" 2003."},{"key":"e_1_3_2_1_6_1","unstructured":"ISO\/IEC 14882:2011 \"Programming languages - C++\" 2011.  ISO\/IEC 14882:2011 \"Programming languages - C++\" 2011."},{"key":"e_1_3_2_1_7_1","volume-title":"ISO\/IEC TR 24772:2013 \"Guidance to avoiding vulnerabilities in programming languages through language selection and use\"","unstructured":"ISO\/IEC TR 24772:2013 \"Guidance to avoiding vulnerabilities in programming languages through language selection and use\" , second edition. ISO\/IEC TR 24772:2013 \"Guidance to avoiding vulnerabilities in programming languages through language selection and use\", second edition."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.44"},{"key":"e_1_3_2_1_9_1","volume-title":"RTCA","author":"RTCA.","year":"2011","unstructured":"RTCA. DO-332 Object-Oriented Technology and Related Techniques Supplement to DO-178C and DO-278A , RTCA , 2011 . RTCA. DO-332 Object-Oriented Technology and Related Techniques Supplement to DO-178C and DO-278A, RTCA, 2011."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111064"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926394"},{"key":"e_1_3_2_1_13_1","unstructured":"IEEE 754-2008 \"IEEE Standard for Floating-Point Arithmetic\" ISBN 978-0-7381-5752-8 2008.  IEEE 754-2008 \"IEEE Standard for Floating-Point Arithmetic\" ISBN 978-0-7381-5752-8 2008."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-585-27524-6_8"},{"key":"e_1_3_2_1_15_1","volume-title":"INRIA & LRI","author":"Moy Yannick","year":"2011","unstructured":"Moy , Yannick , and Claude March\u00e9 . \" The Jessie plugin for Deduction Verification in Frama-C - Tutorial and Reference Manual . INRIA & LRI , 2011 .\" Moy, Yannick, and Claude March\u00e9. \"The Jessie plugin for Deduction Verification in Frama-C - Tutorial and Reference Manual. INRIA & LRI, 2011.\""},{"key":"e_1_3_2_1_16_1","volume-title":"31st International Conference on. IEEE","author":"Dahlweid Markus","year":"2009","unstructured":"Dahlweid , Markus , et al. \" VCC : Contract-based modular verification of concurrent C.\" Software Engineering-Companion Volume, 2009. ICSE-Companion 2009 . 31st International Conference on. IEEE , 2009 . Dahlweid, Markus, et al. \"VCC: Contract-based modular verification of concurrent C.\" Software Engineering-Companion Volume, 2009. ICSE-Companion 2009. 31st International Conference on. IEEE, 2009."},{"key":"e_1_3_2_1_17_1","first-page":"9781848213630","article-title":"Escher Verification Studio: Perfect Developer and Escher C Verifier","author":"Carlton Judith","year":"2013","unstructured":"Carlton , Judith , and David Crocker . \" Escher Verification Studio: Perfect Developer and Escher C Verifier .\" Industrial Use of Formal Methods: Formal Verification: 155--193 , 2013 . ISBN 13: 9781848213630 Carlton, Judith, and David Crocker. \"Escher Verification Studio: Perfect Developer and Escher C Verifier.\" Industrial Use of Formal Methods: Formal Verification: 155--193, 2013. ISBN 13: 9781848213630","journal-title":"Industrial Use of Formal Methods: Formal Verification: 155--193"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986314"},{"key":"e_1_3_2_1_19_1","volume-title":"Technische Universit\u00e4t Wien, 2011","author":"Rainer-Harbach Marian","year":"2014","unstructured":"Rainer-Harbach , Marian . \" Methods and Tools for the Formal Verification of Software \", Technische Universit\u00e4t Wien, 2011 . Retrieved from http:\/\/aragorn.ads.tuwien.ac.at\/publications\/bib\/pdf\/rainer-harbach_11.pdf , 12 June 2014 . Rainer-Harbach, Marian. \"Methods and Tools for the Formal Verification of Software\", Technische Universit\u00e4t Wien, 2011. Retrieved from http:\/\/aragorn.ads.tuwien.ac.at\/publications\/bib\/pdf\/rainer-harbach_11.pdf, 12 June 2014."},{"key":"e_1_3_2_1_20_1","volume-title":"the verified design-by-contract paradigm.\" Proceedings of the Twelfth Safety-Critical Systems Symposium","author":"Crocker David","year":"2004","unstructured":"Crocker , David . \"Safe object-oriented software : the verified design-by-contract paradigm.\" Proceedings of the Twelfth Safety-Critical Systems Symposium (ed. F. Redmill & T. Anderson) 19--41, Springer-Verlag , London , 2004 . ISBN 1-85233-800-8. Crocker, David. \"Safe object-oriented software: the verified design-by-contract paradigm.\" Proceedings of the Twelfth Safety-Critical Systems Symposium (ed. F. Redmill & T. Anderson) 19--41, Springer-Verlag, London, 2004. ISBN 1-85233-800-8."},{"key":"e_1_3_2_1_21_1","volume-title":"section 7.1.2.","author":"Reference Manual","year":"2014","unstructured":"Spark 2014 Reference Manual , section 7.1.2. Retrieved from http:\/\/docs.adacore.com\/spark2014-docs\/html\/lrm\/packages.html#external-state, 31 August 2014 . Spark 2014 Reference Manual, section 7.1.2. Retrieved from http:\/\/docs.adacore.com\/spark2014-docs\/html\/lrm\/packages.html#external-state, 31 August 2014."},{"key":"e_1_3_2_1_22_1","volume-title":"retrieved","year":"2014","unstructured":"http:\/\/www.ncl.ac.uk\/computing\/research\/project\/4519 , retrieved 31 August 2014 . http:\/\/www.ncl.ac.uk\/computing\/research\/project\/4519, retrieved 31 August 2014."}],"event":{"name":"HILT '14: High Integrity Language Technology ACM SIGAda Annual Conference","location":"Portland Oregon USA","acronym":"HILT '14","sponsor":["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","Ada Europe Ada Europe","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 2014 ACM SIGAda annual conference on High integrity language technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2663171.2663179","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2663171.2663179","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:47Z","timestamp":1750212827000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2663171.2663179"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,18]]},"references-count":22,"alternative-id":["10.1145\/2663171.2663179","10.1145\/2663171"],"URL":"https:\/\/doi.org\/10.1145\/2663171.2663179","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2692956.2663179","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,10,18]]},"assertion":[{"value":"2014-10-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}