{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:35Z","timestamp":1725516515034},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_29","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"268-276","source":"Crossref","is-referenced-by-count":2,"title":["A Mechanized Program Verifier"],"prefix":"10.1007","author":[{"given":"J. Strother","family":"Moore","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Bevier, W.R.: A verified operating system kernel. Ph.d. dissertation, University of Texas at Austin (1987)"},{"issue":"4","key":"29_CR2","first-page":"409","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: Special issue on system verification. Journal of Automated Reasoning\u00a05(4), 409\u2013530 (1989)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"29_CR3","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/321864.321875","volume":"22","author":"R.S. Boyer","year":"1975","unstructured":"Boyer, R.S., Moore, J.S.: Proving theorems about pure lisp functions. J. ACM\u00a022(1), 129\u2013144 (1975)","journal-title":"J. ACM"},{"key":"29_CR4","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979)"},{"issue":"3","key":"29_CR5","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1145\/828.1882","volume":"31","author":"R.S. Boyer","year":"1984","unstructured":"Boyer, R.S., Moore, J.S.: A mechanical proof of the unsolvability of the halting problem. Journal of the Association for Computing Machinery\u00a031(3), 441\u2013458 (1984)","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"3","key":"29_CR6","doi-asserted-by":"publisher","first-page":"181","DOI":"10.2307\/2322356","volume":"91","author":"R.S. Boyer","year":"1984","unstructured":"Boyer, R.S., Moore, J.S.: Proof checking the rsa public key encryption algorithm. American Mathematical Monthly\u00a091(3), 181\u2013189 (1984)","journal-title":"American Mathematical Monthly"},{"key":"29_CR7","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-94-011-3488-0_5","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"R.S. Boyer","year":"1991","unstructured":"Boyer, R.S., Moore, J.S.: Mjrty \u2013 a fast majority vote algorithm. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 105\u2013117. Kluwer Academic Publishers, Automated Reasoning Series, Dordrecht (1991)"},{"key":"29_CR8","volume-title":"A Computational Logic Handbook, Second Edition","author":"R.S. Boyer","year":"1997","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, Second Edition. Academic Press, New York (1997)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45587-6_3","volume-title":"Practical Aspects of Declarative Languages","author":"R.S. Boyer","year":"2002","unstructured":"Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol.\u00a02257, Springer, Heidelberg (2002), \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/stobj\/main.ps.gz"},{"key":"29_CR10","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-1-4612-4476-9_7","volume-title":"Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra","author":"R.S. Boyer","year":"1990","unstructured":"Boyer, R.S., Moore, J.S., Green, M.W.: The use of a formal simulator to verify a simple real time control program. In: Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra, pp. 54\u201366. Springer, Heidelberg (1990) (Texts and Monographs in Computer Science)"},{"issue":"1","key":"29_CR11","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"R.S. Boyer","year":"1996","unstructured":"Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. Journal of the ACM\u00a043(1), 166\u2013192 (1996)","journal-title":"Journal of the ACM"},{"key":"29_CR12","volume-title":"Industrial-Strength Formal Methods","author":"B. Brock","year":"1999","unstructured":"Brock, B., Hunt Jr., W.A.: Formal analysis of the motorola CAP DSP. In: Industrial-Strength Formal Methods, Springer, Heidelberg (1999)"},{"key":"29_CR13","volume-title":"Engineering Theories of Software Intensive Systems","author":"B. Brock","year":"2005","unstructured":"Brock, B., Moore, J.S.: A mechanically checked proof of a comparator sort algorithm. In: Engineering Theories of Software Intensive Systems, IOS Press, Amsterdam (to appear, 2005)"},{"key":"29_CR14","unstructured":"Flatau, A.D.: A verified implementation of an applicative language with dynamic storage allocation. Ph.d. thesis, University of Texas at Austin (1992)"},{"key":"29_CR15","unstructured":"Goldberg, J., Kautz, W., Mellear-Smith, P.M., Green, M., Levitt, K., Schwartz, R., Weinstock, C.: Development and analysis of the software implemented fault-tolerance (sift) computer. Technical Report NASA Contractor Report 172146, NASA Langley Research Center, Hampton, VA (1984)"},{"key":"29_CR16","unstructured":"Greve, D., Wilding, M.: Evaluatable, high-assurance microprocessors. In: NSA High-Confidence Systems and Software Conference (HCSS), Linthicum, MD (March 2002), \n                    \n                      http:\/\/hokiepokie.org\/docs\/hcss02\/proceedings.pdf"},{"key":"29_CR17","unstructured":"Greve, D., Wilding, M.: A separation kernel formal security policy (2003)"},{"key":"29_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-49519-3_21","volume-title":"Formal Methods in Computer-Aided Design","author":"D.A. Greve","year":"1998","unstructured":"Greve, D.A.: Symbolic simulation of the JEM1 microprocessor. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 203\u2013203. Springer, Heidelberg (1998)"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57960-5","volume-title":"FM8501: A Verified Microprocessor","author":"W.A. Hunt","year":"1994","unstructured":"Hunt, W.A.: FM8501: A Verified Microprocessor. LNCS, vol.\u00a0795. Springer, Heidelberg (1994)"},{"key":"29_CR20","unstructured":"Hunt, W.A., Brock, B.: A formal HDL and its use in the FM9001 verification. In: Proceedings of the Royal Society (April 1992)"},{"key":"29_CR21","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)"},{"issue":"1","key":"29_CR22","first-page":"181","volume":"98","author":"M. Kaufmann","year":"2004","unstructured":"Kaufmann, M., Moore, J.S.: Some key research problems in automated theorem proving for hardware and software verification. Revista de la Real Academia de Ciencias (RACSAM)\u00a098(1), 181\u2013196 (2004)","journal-title":"Revista de la Real Academia de Ciencias (RACSAM)"},{"key":"29_CR23","unstructured":"Kaufmann, M., Moore, J.S.: The ACL2 home page. In: Dept. of Computer Sciences, University of Texas at Austin (2006), \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/"},{"key":"29_CR24","volume-title":"The C Programming Language, Second Edition","author":"B.W. Kernighan","year":"1988","unstructured":"Kernighan, B.W., Ritchie, D.M.: The C Programming Language, Second Edition. Prentice Hall, Englewood Cliff (1988)"},{"key":"29_CR25","volume-title":"Workshop on Interpreters, Virtual Machines and Emulators 2003 (IVME 2003)","author":"H. Liu","year":"2003","unstructured":"Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: A study. In: Workshop on Interpreters, Virtual Machines and Emulators 2003 (IVME 2003), San Diego, CA, ACM SIGPLAN, New York (2003)"},{"key":"29_CR26","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-1-4757-3188-0_16","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"W. McCune","year":"2000","unstructured":"McCune, W., Shumsky, O.: Ivy: A preprocessor and proof checker for first-order logic. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, Boston, MA, pp. 265\u2013282. Kluwer Academic Press, Dordrecht (2000)"},{"key":"29_CR27","volume-title":"Automated Reasoning Series","author":"J.S. Moore","year":"1996","unstructured":"Moore, J.S.: Piton: A Mechanically Verified Assembly-Level Language. In: Automated Reasoning Series, Kluwer Academic Publishers, Dordrecht (1996)"},{"key":"29_CR28","first-page":"227","volume-title":"Models, Algebras and Logic of Engineering Software","author":"J.S. Moore","year":"2003","unstructured":"Moore, J.S.: Proving theorems about Java and the JVM with ACL2. In: Broy, M., Pizka, M. (eds.) Models, Algebras and Logic of Engineering Software, pp. 227\u2013290. IOS Press, Amsterdam (2003), \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/marktoberdorf-03"},{"issue":"9","key":"29_CR29","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. IEEE Transactions on Computers\u00a047(9), 913\u2013926 (1998)","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"29_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/514188.514189","volume":"24","author":"J.S. Moore","year":"2002","unstructured":"Moore, J.S., Porter, G.: The Apprentice challenge. ACM TOPLAS\u00a024(3), 1\u201324 (2002)","journal-title":"ACM TOPLAS"},{"key":"29_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-30494-4_6","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Ray","year":"2004","unstructured":"Ray, S., Moore, J.S.: Proof styles in operational semantics. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 67\u201381. Springer, Heidelberg (2004)"},{"key":"29_CR32","first-page":"148","volume":"1","author":"D. Russinoff","year":"1998","unstructured":"Russinoff, D.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. London Mathematical Society Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998), \n                    \n                      http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html","journal-title":"London Mathematical Society Journal of Computation and Mathematics"},{"key":"29_CR33","unstructured":"Sawada, J.: Formal verification of divide and square root algorithms using series calculation. In: Proceedings of the ACL2 Workshop, 2002 (April 2002), \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2002"},{"key":"29_CR34","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569883","volume-title":"Metamathematics, Machines, and Godel\u2019s Proof","author":"N. Shankar","year":"1994","unstructured":"Shankar, N.: Metamathematics, Machines, and Godel\u2019s Proof. Cambridge University Press, Cambridge (1994)"},{"key":"29_CR35","unstructured":"Smith, S.W., Austel, V.: Trusting trusted hardware: Towards a formal model for programmable secure coprocessors. In: The Third USENIX Workshop on Electronic Commerce (September 1998)"},{"key":"29_CR36","unstructured":"Sumners, R.: Correctness proof of a BDD manager in the context of satisfiability checking. In: Proceedings of ACL2 Workshop 2000. Department of Computer Sciences, Technical Report TR-00-29 (November 2000), \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2000\/final\/sumners2\/paper.ps"},{"key":"29_CR37","unstructured":"Wilding, M.: Nim game proof. Technical Report CLI Tech Report 249, Computational Logic, Inc. (November 1991), \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/boyer\/ftp\/nqthm\/nqthm-1992\/examples\/numbers\/nim.eventsq"},{"key":"29_CR38","unstructured":"Young, W.D.: A verified code generator for a subset of Gypsy. Technical Report\u00a033, Comp. Logic. Inc. Austin, Texas (1988)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,2]],"date-time":"2019-03-02T12:59:33Z","timestamp":1551531573000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}