{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:17Z","timestamp":1772163977326,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,12,2]],"date-time":"2012-12-02T00:00:00Z","timestamp":1354406400000},"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":[[2012,12,2]]},"DOI":"10.1145\/2402676.2402690","type":"proceedings-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T12:08:34Z","timestamp":1354190914000},"page":"27-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Hi-Lite"],"prefix":"10.1145","author":[{"given":"Johannes","family":"Kanig","sequence":"first","affiliation":[{"name":"AdaCore, Paris, France"}]},{"given":"Edmond","family":"Schonberg","sequence":"additional","affiliation":[{"name":"AdaCore, New York, NY, USA"}]},{"given":"Claire","family":"Dross","sequence":"additional","affiliation":[{"name":"AdaCore, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2012,12,2]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Analysis, design and programming language. Standard ECMA-367, 2d Edition","year":"2006","unstructured":"Eiffel : Analysis, design and programming language. Standard ECMA-367, 2d Edition ( 2006 ). Eiffel : Analysis, design and programming language. Standard ECMA-367, 2d Edition (2006)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_3_2_1_3_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 Longman Publishing Co., Inc. , Boston, MA, USA , 2003 . J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2003."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the First International Workshop on Intermediate Verification Languages","author":"Bobot F.","year":"2011","unstructured":"F. Bobot , J.-C. Filli\u00e2tre , A. Paskevich , and C. March\u00e9 . Why3: Shepherd your herd of provers . In Proceedings of the First International Workshop on Intermediate Verification Languages , Boogie , 2011 . F. Bobot, J.-C. Filli\u00e2tre, A. Paskevich, and C. March\u00e9. Why3: Shepherd your herd of provers. In Proceedings of the First International Workshop on Intermediate Verification Languages, Boogie, 2011."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/978-3-642-20398-5_35","volume-title":"Proceedings of the Third international conference on NASA Formal methods, NFM'11","author":"Cok D. R.","year":"2011","unstructured":"D. R. Cok . OpenJML : JML for Java 7 by extending OpenJDK . In Proceedings of the Third international conference on NASA Formal methods, NFM'11 , pages 472 -- 479 , Berlin, Heidelberg , 2011 . Springer-Verlag. D. R. Cok. OpenJML: JML for Java 7 by extending OpenJDK. In Proceedings of the Third international conference on NASA Formal methods, NFM'11, pages 472--479, Berlin, Heidelberg, 2011. Springer-Verlag."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the Embedded Real Time Software and Systems conference, ERTS$^2$ 2012","author":"Comar C.","year":"2012","unstructured":"C. Comar , J. Kanig , and Y. Moy . Integrating formal program verification with testing . In Proceedings of the Embedded Real Time Software and Systems conference, ERTS$^2$ 2012 , Feb. 2012 . C. Comar, J. Kanig, and Y. Moy. Integrating formal program verification with testing. In Proceedings of the Embedded Real Time Software and Systems conference, ERTS$^2$ 2012, Feb. 2012."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.44"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_2_1_13_1","volume-title":"Predicate Calculus and Program Semantics","author":"Dijsktra E.","year":"1989","unstructured":"E. Dijsktra and C. Sholten . Predicate Calculus and Program Semantics . Springer , New York , Berlin, 1989 . E. Dijsktra and C. Sholten. Predicate Calculus and Program Semantics. Springer, New York, Berlin, 1989."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2025936.2025945"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TOPI.2012.6229809"},{"key":"e_1_3_2_1_17_1","unstructured":"Hi-Lite: Simplifying the use of formal methods. http:\/\/www.open-do.org\/projects\/hi-lite\/.  Hi-Lite: Simplifying the use of formal methods. http:\/\/www.open-do.org\/projects\/hi-lite\/."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_5"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1417069"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_49"},{"key":"e_1_3_2_1_23_1","volume-title":"SAnToS Laboratory","author":"Chalin P.","year":"2009","unstructured":"Robby and P. Chalin . Preliminary design of a unified JML representation and software infrastructure. Technical report , SAnToS Laboratory , Kansas State University , 2009 . Robby and P. Chalin. Preliminary design of a unified JML representation and software infrastructure. Technical report, SAnToS Laboratory, Kansas State University, 2009."},{"key":"e_1_3_2_1_24_1","volume-title":"A Guide to Learning the Testbench Language Features","author":"Spear C.","year":"2008","unstructured":"C. Spear . SystemVerilog for Verification : A Guide to Learning the Testbench Language Features . Springer , New York , Berlin, 2008 . C. Spear. SystemVerilog for Verification: A Guide to Learning the Testbench Language Features. Springer, New York, Berlin, 2008."}],"event":{"name":"HILT'12: ACM SIGAda Annual","location":"Boston Massachusetts USA","acronym":"HILT'12","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","SIGBED ACM Special Interest Group on Embedded Systems","SIGCAS ACM Special Interest Group on Computers and Society","SIGCSE ACM Special Interest Group on Computer Science Education"]},"container-title":["Proceedings of the 2012 ACM conference on High integrity language technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2402676.2402690","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2402676.2402690","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:12Z","timestamp":1750225692000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2402676.2402690"}},"subtitle":["the convergence of compiler technology and program verification"],"short-title":[],"issued":{"date-parts":[[2012,12,2]]},"references-count":24,"alternative-id":["10.1145\/2402676.2402690","10.1145\/2402676"],"URL":"https:\/\/doi.org\/10.1145\/2402676.2402690","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2402709.2402690","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2012,12,2]]},"assertion":[{"value":"2012-12-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}