{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:34Z","timestamp":1750308574903,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T00:00:00Z","timestamp":1497830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1161916"],"award-info":[{"award-number":["CCF-1161916"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,6,19]]},"DOI":"10.1145\/3098572.3098580","type":"proceedings-article","created":{"date-parts":[[2017,6,28]],"date-time":"2017-06-28T12:30:41Z","timestamp":1498653041000},"page":"1-3","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalization IDEs Integrated with a Verifying Compiler"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Welch","sequence":"first","affiliation":[{"name":"School of Computing, Clemson University, Clemson, SC, USA"}]},{"given":"Blair","family":"Durkee","sequence":"additional","affiliation":[{"name":"School of Computing, Clemson University, Clemson, SC, USA"}]},{"given":"Mike","family":"Kabbani","sequence":"additional","affiliation":[{"name":"School of Computing, Clemson University, Clemson, SC, USA"}]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[{"name":"School of Computing, Clemson University, Clemson, SC, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,6,19]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Lecture Notes in Computer Science","volume":"10001","author":"Ahrendt Wolfgang","year":"2016"},{"volume-title":"ICSE","year":"2012","author":"Cook C. T.","key":"e_1_3_2_1_2_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1145\/2716316"},{"unstructured":"Heather Harton. 2011. Mechanical and Modular Verification Condition Generation For Object-Based Software. Ph.D. Dissertation. Clemson University.   Heather Harton. 2011. Mechanical and Modular Verification Condition Generation For Object-Based Software. Ph.D. Dissertation. Clemson University.","key":"e_1_3_2_1_4_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1007\/978-3-319-10181-1_4"},{"unstructured":"JetBrains. 2017. IDEs. Software https:\/\/www.jetbrains.com\/. (2017).  JetBrains. 2017. IDEs. Software https:\/\/www.jetbrains.com\/. (2017).","key":"e_1_3_2_1_6_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.5555\/2075679.2075711"},{"unstructured":"Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel M. Zimmerman and Werner Dietl. 2013. JML Reference Manual. Revision 2344.  Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel M. Zimmerman and Werner Dietl. 2013. JML Reference Manual. Revision 2344.","key":"e_1_3_2_1_8_1"},{"volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR 2010 (LNCS), Edmund M","year":"2010","author":"Leino K. Rustan M.","key":"e_1_3_2_1_9_1"},{"unstructured":"K. Rustan M. Leino and Philipp R\u00fcmmer. 2014. The Dafny Integrated Development Environment. In F-IDE 2014 (EPTCS) Catherine Dubois Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.) Vol. 149. EPTCS 3--15.  K. Rustan M. Leino and Philipp R\u00fcmmer. 2014. The Dafny Integrated Development Environment. In F-IDE 2014 (EPTCS) Catherine Dubois Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.) Vol. 149. EPTCS 3--15.","key":"e_1_3_2_1_10_1"},{"doi-asserted-by":"crossref","unstructured":"Nadia Polikarpova Julian Tschannen and Carlo A. Furia. 2015. A Fully Verified Container Library. Springer Cham 414--434.  Nadia Polikarpova Julian Tschannen and Carlo A. Furia. 2015. A Fully Verified Container Library. Springer Cham 414--434.","key":"e_1_3_2_1_11_1","DOI":"10.1007\/978-3-319-19249-9_26"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1007\/s00165-010-0154-3"},{"unstructured":"Hampton Smith. 2013. Engineering Specifications and Mathematics for Verified Software. Ph.D. Dissertation. Clemson University.  Hampton Smith. 2013. Engineering Specifications and Mathematics for Verified Software. Ph.D. Dissertation. Clemson University.","key":"e_1_3_2_1_13_1"},{"unstructured":"The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual. V8.6.  The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual. V8.6.","key":"e_1_3_2_1_14_1"},{"volume-title":"Verifying Eiffel Programs with Boogie. In First International Workshop on Intermediate Verification Languages, BOOGIE","year":"2011","author":"Tschannen Julian","key":"e_1_3_2_1_15_1"},{"key":"e_1_3_2_1_16_1","volume-title":"Engineering and Employing Reusable Software Components for Modular Verification. In ICSR 2017 (In publication) (LNCS), Goetz Botterweck and Claudia Werner (Eds.)","volume":"10221","author":"Welch Daniel","year":"2017"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","AITO Assoc Internationale por les Technologies Objects"],"acronym":"ECOOP '17","name":"ECOOP '17: European Conference on Object-Oriented Programming","location":"Barcelona Spain"},"container-title":["Proceedings of the 12th Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3098572.3098580","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3098572.3098580","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3098572.3098580","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:04:48Z","timestamp":1750273488000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3098572.3098580"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,19]]},"references-count":16,"alternative-id":["10.1145\/3098572.3098580","10.1145\/3098572"],"URL":"https:\/\/doi.org\/10.1145\/3098572.3098580","relation":{},"subject":[],"published":{"date-parts":[[2017,6,19]]},"assertion":[{"value":"2017-06-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}