{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:44:28Z","timestamp":1725486268679},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651109"},{"type":"electronic","value":"9783540496465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49646-7_17","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T05:09:52Z","timestamp":1181624992000},"page":"221-230","source":"Crossref","is-referenced-by-count":0,"title":["A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools"],"prefix":"10.1007","author":[{"given":"Piergiorgio","family":"Bertoli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fausto","family":"Giunchiglia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Traverso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,12,14]]},"reference":[{"key":"17_CR1","volume-title":"PhD thesis","author":"P.G. Bertoli","year":"1998","unstructured":"P.G. Bertoli. Using OMRS in practice: a case study with acl2. PhD thesis, Computer Science Dept., University Rome 3, Rome, 1998. Forthcoming."},{"doi-asserted-by":"crossref","unstructured":"A. Cimatti, F. Giunchiglia, P. Pecchiari, B. Pietra, J. Profeta, D. Romano, and P. Traverso. A Provably Correct Embedded Verifier for the Certification of Safety Critical Software. In Proc. Computer-Aided Verification (CAV\u201997), Haifa, Israel, June 1997.","key":"17_CR2","DOI":"10.1007\/3-540-63166-6_21"},{"doi-asserted-by":"crossref","unstructured":"F. Giunchiglia, P. Pecchiari, and C. Talcott. Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. Technical Report 9409-15, IRST, Trento, Italy, 1994. Short version published in Proc. of the First International Workshop on Frontiers of Combining Systems (FroCoS\u201996), Munich, Germany, March 1996.","key":"17_CR3","DOI":"10.1007\/978-94-009-0349-4_8"},{"doi-asserted-by":"crossref","unstructured":"M.J. Gordon. A Proof Generating System for Higher-Order Logic. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification and Synthesis. Kluwer, 1987.","key":"17_CR4","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"17_CR5","volume-title":"Tech. Report ORA TM-95-0081","author":"D. Guaspari","year":"1995","unstructured":"D. Guaspari, C. Barbash, and D. Hoover. Checking critical code. Tech. Report ORA TM-95-0081, Odyssey Research Associates, Ithaca, USA, September 1995."},{"unstructured":"M. Kaufmann and J. S. Moore. acl2 Version 1.8 User\u2019s Manual. Available on line at http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/index.html .","key":"17_CR6"},{"key":"17_CR7","volume-title":"Technical Report 101","author":"M. Kaufmann","year":"1994","unstructured":"M. Kaufmann and J S. Moore. Design Goals for ACL2. Technical Report 101, Computational Logic Inc., Austin, Texas, 1994."},{"doi-asserted-by":"crossref","unstructured":"S. Kromodimoeljo, B. Pase, M. Saaltink, D. Craigen, and I. Meisels. The EVES system. In Proc. of the Int. Lecture Series on \u201eFunctional Programming, Concurrency, Simulation and Automated Reasoning\u201c. McMaster University, 1992.","key":"17_CR8","DOI":"10.1007\/3-540-56883-2_16"},{"doi-asserted-by":"crossref","unstructured":"G. Necula. Proof-carrying code. In 24th Annual ACM-SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201997), 1997.","key":"17_CR9","DOI":"10.1145\/263699.263712"},{"doi-asserted-by":"crossref","unstructured":"G. Necula and P. Lee. Safe kernel extensions without run-time checking. In Second Symposium on Operating Systems Design and Implementation (OSDI\u201996), 1996.","key":"17_CR10","DOI":"10.1145\/238721.238781"},{"doi-asserted-by":"crossref","unstructured":"Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Proceedings of TACAS\u201998. To appear., 1998.","key":"17_CR11","DOI":"10.1007\/BFb0054170"},{"issue":"11","key":"17_CR12","first-page":"54","volume":"29","author":"J. Profeta","year":"1996","unstructured":"J. Profeta, N. Andrianos, B. Yu, B. Jonson, T. DeLong, D. Guaspari, and D. Jamsek. Safety Critical Systems Built with COTS. Computer, 29(11):54\u201360, November 1996.","journal-title":"Safety Critical Systems Built with COTS. Computer"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49646-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,23]],"date-time":"2020-04-23T01:57:22Z","timestamp":1587607042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49646-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651109","9783540496465"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-49646-7_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}