{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:52:23Z","timestamp":1772121143155,"version":"3.50.1"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/hase.2004.1281741","type":"proceedings-article","created":{"date-parts":[[2004,6,10]],"date-time":"2004-06-10T14:19:45Z","timestamp":1086877185000},"page":"167-177","source":"Crossref","is-referenced-by-count":4,"title":["The SSP: an example of high-assurance systems engineering"],"prefix":"10.1109","author":[{"given":"G.L.","family":"Wickstrom","sequence":"first","affiliation":[]},{"given":"J.","family":"Davis","sequence":"additional","affiliation":[]},{"given":"S.E.","family":"Morrison","sequence":"additional","affiliation":[]},{"given":"S.","family":"Roach","sequence":"additional","affiliation":[]},{"given":"V.L.","family":"Winter","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","article-title":"Mechanized formal reasoning about programs and computing machines","author":"moore","year":"1996","journal-title":"Automated Reasoning and Its Applications Essays in Honor of Larry Wos"},{"key":"17","first-page":"139","article-title":"Proving theorem about java-like byte code","volume":"1710","author":"moore","year":"1999","journal-title":"LNCS"},{"key":"18","first-page":"227","article-title":"Proving theorems about java and the JVM with ACL2","author":"moore","year":"2003","journal-title":"Models Algebras and Logic of Engineering Software"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2000.895448"},{"key":"16","author":"moore","year":"1996","journal-title":"Piton A mechanically verified assembly-language"},{"key":"13","author":"la?mmel","year":"0","journal-title":"The Essence of Strategic Programming"},{"key":"14","author":"lindholm","year":"1999","journal-title":"Java Virtual Machine Specification 2nd Edition"},{"key":"11","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/382294.382710","article-title":"A reply to the criticisms of the Knight & Leveson experiment","volume":"15","author":"knight","year":"1990","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00028-0"},{"key":"21","first-page":"139","article-title":"Proving theorems about Javalike byte code","volume":"1710","author":"moore","year":"1999","journal-title":"LNCS"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/12.713311"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61512-2"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00298-1"},{"key":"24","article-title":"Language independent traversals for program transformation","author":"visser","year":"2000","journal-title":"Workshop on Generic Programming (WGP'00)"},{"key":"25","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48685-2_3","article-title":"Strategic pattern matching","author":"visser","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"26","year":"0"},{"key":"27","first-page":"35","article-title":"Assuring passive safety in high consequence systems","volume":"31","author":"winter","year":"1998","journal-title":"IEEE Computer"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58002-0"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227603"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82552-6"},{"key":"10","article-title":"A large scale experiment in n-version programming","author":"knight","year":"1985","journal-title":"Digest of Papers FTCS-15 Fifteenth International Symposium on Fault-tolerant Computing"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231893"},{"key":"7","author":"gosling","year":"0","journal-title":"The Java Language Environment A White Paper"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231895"},{"key":"5","first-page":"25","article-title":"Java proving itself worthy for defense apps","author":"child","year":"2003","journal-title":"COTS Journal"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/941566.941568"},{"key":"9","author":"kaufmann","year":"2000","journal-title":"Computer-aided Reasoning Case Studies"},{"key":"8","author":"kaufmann","year":"2000","journal-title":"Computer-Aided Reasoning An Approach"}],"event":{"name":"Eighth IEEE International Symposium on High Assurance Systems Engineering, 2004.","location":"Tampa, FL, USA"},"container-title":["Eighth IEEE International Symposium on High Assurance Systems Engineering, 2004. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9019\/28627\/01281741.pdf?arnumber=1281741","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T07:56:29Z","timestamp":1497599789000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1281741\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/hase.2004.1281741","relation":{},"subject":[]}}