{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:55Z","timestamp":1763468095387,"version":"3.28.0"},"reference-count":23,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,6]]},"DOI":"10.1109\/icse.2012.6227243","type":"proceedings-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T17:24:04Z","timestamp":1341854644000},"page":"1379-1382","source":"Crossref","is-referenced-by-count":13,"title":["Specification engineering and modular verification using a web-integrated verifying compiler"],"prefix":"10.1109","author":[{"given":"Charles T.","family":"Cook","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heather","family":"Harton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hampton","family":"Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","first-page":"364","article-title":"Boogie: A Modular Reusable Verifier for Object-Oriented Programs","volume":"4709","author":"barnet","year":"2006","journal-title":"LNCS"},{"key":"22","article-title":"The KeY tool: Integrating object oriented design and formal verification","volume":"4334","author":"ahrendt","year":"2007","journal-title":"LNCS"},{"journal-title":"A Web-Integrated Environment for Component-Based Software Reasoning","year":"2011","author":"cook","key":"17"},{"journal-title":"Automatic Full Functional Verification of Clients of User-Defined Abstract Data Types","year":"2010","author":"kirschenbaum","key":"23"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_8"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04211-9_4"},{"key":"16","article-title":"Integrating Math Units and Proof Checking for Specification and Verification","author":"smith","year":"0","journal-title":"7th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008)"},{"key":"13","first-page":"49","article-title":"The Spec# Programming System: An Overview","volume":"3362","author":"barnet","year":"2004","journal-title":"LNCS"},{"key":"14","first-page":"348","article-title":"Dafny: An automatic program verifier for functional correctness","author":"rustan","year":"2010","journal-title":"Proc 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1002\/9780470050118.ecse331"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0164-8"},{"key":"3","article-title":"Isabelle\/HOL - A Proof Assistant for Higher- Order Logic","volume":"2283","author":"nipkow","year":"2002","journal-title":"LNCS"},{"key":"20","first-page":"304","article-title":"A Quick Tour of the VeriFast Program Verifier","volume":"6461","author":"jacobs","year":"2010","journal-title":"LNCS"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0154-3"},{"year":"2012","key":"1"},{"key":"10","first-page":"53","article-title":"A Case Study in Automated Verification","author":"kirschenbaum","year":"2008","journal-title":"Proc AFM'08 3rd Workshop on Automated Formal Methods"},{"journal-title":"To Expand or Not to Expand Automatically Verifying Software Specified with Complex Mathematical Definitions","year":"2011","author":"tagore","key":"7"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_10"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2006.1639580"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04211-9_2"},{"key":"9","article-title":"The 1st Verified Software Competition: Experience Report","volume":"6664","author":"muller","year":"2011","journal-title":"LNCS"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_4"}],"event":{"name":"2012 34th International Conference on Software Engineering (ICSE 2012)","start":{"date-parts":[[2012,6,2]]},"location":"Zurich","end":{"date-parts":[[2012,6,9]]}},"container-title":["2012 34th International Conference on Software Engineering (ICSE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6218989\/6227015\/06227243.pdf?arnumber=6227243","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,21]],"date-time":"2017-03-21T16:08:44Z","timestamp":1490112524000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6227243\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":23,"URL":"https:\/\/doi.org\/10.1109\/icse.2012.6227243","relation":{},"subject":[],"published":{"date-parts":[[2012,6]]}}}