{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:36Z","timestamp":1772164056060,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":16,"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.2534188","type":"proceedings-article","created":{"date-parts":[[2013,11,12]],"date-time":"2013-11-12T10:29:36Z","timestamp":1384252176000},"page":"7-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Practical specification and verification with code contracts"],"prefix":"10.1145","author":[{"given":"Francesco","family":"Logozzo","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, Washington, USA"}]}],"member":"320","published-online":{"date-parts":[[2013,11,10]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"Barnes J.","year":"2003","unstructured":"J. Barnes . High Integrity Software: The SPARK Approach to Safety and Security . Addison-Wesley , 2003 . J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, 2003."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1774088.1774531"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_13"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926399"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TOPI.2012.6229809"},{"key":"e_1_3_2_1_9_1","volume-title":"FoVeOOS","author":"F\u00e4hndrich M.","year":"2010","unstructured":"M. F\u00e4hndrich and F. Logozzo . Static contract checking with abstract interpretation . In FoVeOOS , 2010 . M. F\u00e4hndrich and F. Logozzo. Static contract checking with abstract interpretation. In FoVeOOS, 2010."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449791"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_20"},{"key":"e_1_3_2_1_12_1","volume-title":"CAV","author":"Leavens G. T.","year":"2007","unstructured":"G. T. Leavens , J. R. Kiniry , and E. Poll . A jml tutorial: Modular specification and verification of functional behavior for java . In CAV , 2007 . G. T. Leavens, J. R. Kiniry, and E. Poll. A jml tutorial: Modular specification and verification of functional behavior for java. In CAV, 2007."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384626"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1363686.1363736"},{"key":"e_1_3_2_1_15_1","volume-title":"Eiffel: The Language","author":"Meyer B.","year":"1991","unstructured":"B. Meyer . Eiffel: The Language . Prentice Hall , 1991 . B. Meyer. Eiffel: The Language. Prentice Hall, 1991."},{"key":"e_1_3_2_1_16_1","unstructured":"Microsoft. Codecontracts tools.texttthttp:\/\/aka.ms\/codecontracts\/vsgallery.  Microsoft. Codecontracts tools.texttthttp:\/\/aka.ms\/codecontracts\/vsgallery."}],"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.2534188","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2527269.2534188","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:34:29Z","timestamp":1750217669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2527269.2534188"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11,10]]},"references-count":16,"alternative-id":["10.1145\/2527269.2534188","10.1145\/2527269"],"URL":"https:\/\/doi.org\/10.1145\/2527269.2534188","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2658982.2534188","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"}}]}}