{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T07:10:48Z","timestamp":1791357048736,"version":"4.3.1"},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,6]]},"DOI":"10.1109\/icse.2012.6227120","type":"proceedings-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T17:24:04Z","timestamp":1341854644000},"page":"1002-1011","source":"Crossref","is-referenced-by-count":21,"title":["Large-scale formal verification in practice: A process perspective"],"prefix":"10.1109","author":[{"given":"June","family":"Andronick","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ross","family":"Jeffery","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rafal","family":"Kolanski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Staples","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"He","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Liming","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"19","article-title":"Formal specification techniques in the commercial development process","author":"fitzgerald","year":"0","journal-title":"Position Papers from the Workshop on Formal Methods Application in Software Engineering Practice ICSE-17 1995"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1109\/52.391826"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/52.57891"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"15","first-page":"170","article-title":"Managerial issues for the consideration and use of formal methods","volume":"2805","author":"stidolph","year":"2003","journal-title":"LNCS"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9123-z"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/METRIC.1997.637174"},{"key":"14","author":"wheeler","year":"2001","journal-title":"SLOCCount"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72426-1_5"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/52.493020"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.1993.346058"},{"key":"23","first-page":"325","article-title":"SeL4 enforces integrity","volume":"6898","author":"sewell","year":"2011","journal-title":"LNCS"},{"key":"24","first-page":"1395","article-title":"Formal proof - Theory and practice","volume":"55","author":"harrison","year":"2008","journal-title":"Notices of the AMS"},{"key":"25","article-title":"Peer Review of a Formal Verification\/Design Proof Methodology","year":"1983","journal-title":"NASA Conference Publication 2377"},{"key":"26","first-page":"207","article-title":"Formal methods: Why should I care? - The development of the T800 transputer floating-point unit","author":"gibbons","year":"0","journal-title":"Proceedings 13th New Zealand Computer Society Conference 1993"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"28","first-page":"500","article-title":"Mind the gap: A verification framework for low-level C","volume":"5674","author":"winwood","year":"2009","journal-title":"LNCS"},{"key":"29","author":"cohn","year":"1987","journal-title":"A Proof of Correctness of the Viper Microprocessor The First Level"},{"key":"3","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1145\/196244.196392","article-title":"fitting formal methods into the design cycle","author":"mcmillan","year":"1994","journal-title":"31st Design Automation Conference"},{"key":"2","year":"2009","journal-title":"Common Criteria for Information Technology Security Evaluation Version 3 1 Revision 3"},{"key":"10","first-page":"530","article-title":"Symbolic simulation: An ACL2 approach","volume":"1522","author":"strother moore","year":"1998","journal-title":"LNCS"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596566"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159850"},{"key":"32","doi-asserted-by":"crossref","DOI":"10.21236\/AD0785072","author":"milner","year":"1972","journal-title":"Logic for Computable Functions Description of a Machine Implementation"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79707-4_7"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/234215.234473"},{"key":"9","article-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","volume":"2283","author":"nipkow","year":"2002","journal-title":"LNCS"},{"key":"8","author":"brooks","year":"2010","journal-title":"The Design of Design Essays from A Computer Scientist"}],"event":{"name":"2012 34th International Conference on Software Engineering (ICSE 2012)","location":"Zurich","start":{"date-parts":[[2012,6,2]]},"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\/06227120.pdf?arnumber=6227120","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,30]],"date-time":"2019-06-30T15:07:14Z","timestamp":1561907234000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6227120\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/icse.2012.6227120","relation":{},"subject":[],"published":{"date-parts":[[2012,6]]}}}