{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:51:09Z","timestamp":1743040269520,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":58,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781441915382"},{"type":"electronic","value":"9781441915399"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-4419-1539-9_1","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T00:26:11Z","timestamp":1267489571000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["ACL2 and Its Applications to Digital System Verification"],"prefix":"10.1007","author":[{"given":"Matt","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,1,23]]},"reference":[{"issue":"4","key":"1_CR1_1","first-page":"409","volume":"5","author":"W Bevier","year":"1989","unstructured":"Bevier W, Hunt WA Jr, Moore JS, Young W (1989) Special issue on system verification. J Autom Reason 5(4):409\u2013530","journal-title":"J Autom Reason"},{"key":"1_CR2_1","volume-title":"A computational logic","author":"RS Boyer","year":"1979","unstructured":"Boyer RS, Moore JS (1979) A computational logic. Academic, New York"},{"key":"1_CR3_1","volume-title":"The correctness problem in computer science","author":"RS Boyer","year":"1981","unstructured":"Boyer RS, Moore JS (1981) Metafunctions: proving them correct and using them efficiently as new proof procedures. In: Boyer RS, Moore JS (eds) The correctness problem in computer science. Academic, London"},{"key":"1_CR4_1","volume-title":"A computational logic handbook","author":"RS Boyer","year":"1997","unstructured":"Boyer RS, Moore JS (1997) A computational logic handbook, 2nd edn. Academic, New York","edition":"2"},{"key":"1_CR5_1","series-title":"PADL 2002, LNCS 2257","first-page":"9","volume-title":"Single-threaded objects in ACL2","author":"RS Boyer","year":"2002","unstructured":"Boyer RS, Moore JS (2002) Single-threaded objects in ACL2. In: PADL 2002, LNCS 2257. Springer, Heidelberg, pp 9\u201327. http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/stobj\/main.ps.gz"},{"issue":"1","key":"1_CR6_1","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"RS Boyer","year":"1996","unstructured":"Boyer RS, Yu Y (1996) Automated proofs of object code for a widely used microprocessor. J ACM 43(1):166\u2013192","journal-title":"J ACM"},{"key":"1_CR7_1","volume-title":"Industrial-strength formal methods","author":"B Brock","year":"1999","unstructured":"Brock B, Hunt WA Jr (1999) Formal analysis of the motorola CAP DSP. In: Hinchey M, Bowen J (eds) Industrial-strength formal methods. Springer, Heidelberg"},{"key":"1_CR8_1","volume-title":"A verified implementation of an applicative language with dynamic storage allocation. PhD thesis","author":"AD Flatau","year":"1992","unstructured":"Flatau AD (1992) A verified implementation of an applicative language with dynamic storage allocation. PhD thesis, University of Texas at Austin"},{"unstructured":"Flatau A, Kaufmann M, Reed D, Russinoff D, Smith E, Sumners R (2002) Formal verification of microprocessors at AMD. In: Proceedings of designing correct circuits 2002. http:\/\/www.cs.chalmers.se\/~ms\/DCC02\/Slides.html","key":"1_CR9_1"},{"doi-asserted-by":"crossref","unstructured":"Goerigk W, Hoffmann U (1998) Rigorous compiler implementation correctness: how to prove the real thing correct. In: Proceedings FM-TRENDS\u201998 international workshop on current trends in applied formal methods, Boppard, LNCS","key":"1_CR10_1","DOI":"10.1007\/3-540-48257-1_7"},{"key":"1_CR11_1","volume-title":"Recursive number theory","author":"RL Goodstein","year":"1964","unstructured":"Goodstein RL (1964) Recursive number theory. North-Holland, Amsterdam"},{"unstructured":"Greve D, Wilding M (2002) Evaluatable, high-assurance microprocessors. In: NSA high-confidence systems and software conference (HCSS), Linthicum, MD. http:\/\/hokiepokie.org\/docs\/hcss02\/proceedings.pdf","key":"1_CR12_1"},{"key":"1_CR13_1","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-1-4757-3188-0_8","volume-title":"Computer-aided reasoning: ACL2 case studies","author":"D Greve","year":"2000","unstructured":"Greve D, Wilding M, Hardin D (2000) High-speed, analyzable simulators. In: Kaufmann M, Manolios P, Moore JS (eds) Computer-aided reasoning: ACL2 case studies. Kluwer, Boston, MA, pp 113\u2013136"},{"unstructured":"Greve D, Wilding M, Vanfleet WM (2003) A separation kernel formal security policy. In: ACL2 workshop 2003, Boulder, CO. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/","key":"1_CR14_1"},{"unstructured":"Greve D, Richards R, Wilding M (2004) A summary of intrinsic partitioning verification. In: ACL2 workshop 2004, Austin, TX. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/","key":"1_CR15_1"},{"unstructured":"Greve D, Wilding M, Richards R, Vanfleet M (2005) Formalizing security policies for dynamic and distributed systems. In: Proceedings of systems and software technology conference (SSTC) 2005, Salt Lake City, UT. http:\/\/hokiepokie.org\/docs\/sstc05.pdf","key":"1_CR16_1"},{"issue":"01","key":"1_CR17_1","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1017\/S0956796807006338","volume":"18","author":"D Greve","year":"2008","unstructured":"Greve D, Kaufmann M, Manolios P, Moore JS, Ray S, Ruiz-Reina JL, Sumners R, Vroon D, Wilding M (2008) Efficient execution in an automated reasoning environment. J Funct Program 18(01):15\u201346","journal-title":"J Funct Program"},{"doi-asserted-by":"crossref","unstructured":"Hardin D, Wilding M, Greve D (1998) Transforming the theorem prover into a digital design tool: from concept car to off-road vehicle. In: Hu AJ, Vardi MY (eds) Computer-aided verification \u2013 CAV \u201998, Lecture notes in computer science, vol 1427. Springer, Heidelberg. See http:\/\/pobox.com\/users\/hokie\/docs\/concept.ps","key":"1_CR18_1","DOI":"10.1007\/BFb0028729"},{"key":"1_CR19_1","series-title":"ACL2 \u201906: proceedings of the sixth international workshop on the ACL2 theorem prover and its applications","first-page":"11","volume-title":"A robust machine code proof framework for highly secure applications","author":"DS Hardin","year":"2006","unstructured":"Hardin DS, Smith EW, Young WD (2006) A robust machine code proof framework for highly secure applications. In: ACL2 \u201906: proceedings of the sixth international workshop on the ACL2 theorem prover and its applications. ACM, New York, NY, pp 11\u201320. DOI http:\/\/doi.acm.org\/10.1145\/1217975.1217978"},{"key":"1_CR20_1","volume-title":"FM8501: a verified microprocessor. LNAI 795","author":"WA Hunt Jr","year":"1994","unstructured":"Hunt WA Jr (1994) FM8501: a verified microprocessor. LNAI 795. Springer, Heidelberg"},{"key":"1_CR21_1","first-page":"151","volume-title":"Computer-aided reasoning: ACL2 case studies","author":"WA Hunt Jr","year":"2000","unstructured":"Hunt WA Jr (2000) The DE language. In: Kaufmann M, Manolios P, Moore JS (eds) Computer-aided reasoning: ACL2 case studies. Kluwer, Boston, MA, pp 151\u2013166"},{"issue":"1652","key":"1_CR22_1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1098\/rsta.1992.0024","volume":"339","author":"WA Hunt Jr","year":"1992","unstructured":"Hunt WA Jr, Brock B (1992) A formal HDL and its use in the FM9001 verification. Philosophical Transactions of the Royal Society: Physical and Engineering Sciences, 339(1652):35\u201347","journal-title":"Philosophical Transactions of the Royal Society: Physical and Engineering Sciences"},{"key":"1_CR23_1","first-page":"163","volume-title":"18th international conference on theorem proving in higher order logics: TPHOLs 2005, Lecture notes in computer science","author":"WA Hunt Jr","year":"2005","unstructured":"Hunt WA Jr, Kaufmann M, Krug RB, Moore JS, Smith EW (2005) Meta reasoning in ACL2. In: Hurd J, Melham T (eds) 18th international conference on theorem proving in higher order logics: TPHOLs 2005, Lecture notes in computer science, vol 3603. Springer, Heidelberg, pp 163\u2013178"},{"unstructured":"Kaufmann M (2008) Aspects of ACL2 User interaction (Invited talk, 8th international workshop on user interfaces for theorem provers (UITP 2008), Montreal, Canada, August, 2008). See www.ags.uni-sb.de\/~omega\/workshops\/UITP08\/kaufmann-UITP08\/talk.html","key":"1_CR24_1"},{"doi-asserted-by":"crossref","unstructured":"Kaufmann M (2009) Abbreviated output for input in ACL2: an implementation case study. In: Proceedings of ACL2 workshop 2009. http:\/\/www.cs.utexas.edu\/users\/sandip\/acl2-09","key":"1_CR25_1","DOI":"10.1145\/1637837.1637847"},{"unstructured":"Kaufmann M, Moore JS (1997) A precise description of the ACL2 logic. Technical report, Deparment of Computer Sciences, University of Texas at Austin. http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/km97a.ps.gz","key":"1_CR26_1"},{"issue":"2","key":"1_CR27_1","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M Kaufmann","year":"2001","unstructured":"Kaufmann M, Moore JS (2001) Structured theory development for a mechanized logic. J Autom Reason 26(2):161\u2013203","journal-title":"J Autom Reason"},{"doi-asserted-by":"crossref","unstructured":"Kaufmann M, Moore JS (2008a) An ACL2 tutorial. In: Proceedings of theorem proving in higher order logics, 21st international conference, TPHOLs 2008. Springer, Heidelberg. See http:\/\/dx.doi.org\/10.1007\/978-3-540-71067-7_4","key":"1_CR28_1","DOI":"10.1007\/978-3-540-71067-7_4"},{"key":"1_CR29_1","series-title":"A Festschrift in honour of Prof. Michael J. C. Gordon FRS","volume-title":"Proof search debugging tools in ACL2","author":"M Kaufmann","year":"2008","unstructured":"Kaufmann M, Moore JS (2008b) Proof search debugging tools in ACL2. In: A Festschrift in honour of Prof. Michael J. C. Gordon FRS. Royal Society, London"},{"unstructured":"Kaufmann M, Moore JS (2009) The ACL2 home page. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/","key":"1_CR30_1"},{"volume-title":"Computer-aided reasoning: ACL2 case studies","year":"2000","unstructured":"Kaufmann M, Manolios P, Moore JS (eds) (2000a) Computer-aided reasoning: ACL2 case studies. Kluwer, Boston, MA","key":"1_CR31_1"},{"key":"1_CR32_1","volume-title":"Computer-aided reasoning: an approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann M, Manolios P, Moore JS (2000b) Computer-aided reasoning: an approach. Kluwer, Boston, MA"},{"issue":"1","key":"1_CR33_1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jal.2007.07.002","volume":"7","author":"M Kaufmann","year":"2009","unstructured":"Kaufmann M, Moore JS, Ray S, Reeber E (2009) Integrating external deduction tools with ACL2. J Appl Logic 7(1):3\u201325","journal-title":"J Appl Logic"},{"unstructured":"Kaufmann M, Moore JS, Ray S (in press) Foundations of automated induction for a structured mechanized logic","key":"1_CR34_1"},{"key":"1_CR35_1","volume-title":"Formal specification and verification of a jvm and its bytecode verifier. PhD thesis","author":"H Liu","year":"2006","unstructured":"Liu H (2006) Formal specification and verification of a jvm and its bytecode verifier. PhD thesis, University of Texas at Austin"},{"key":"1_CR36_1","series-title":"Formal methods in computer-aided design, FMCAD 2000, LNCS 1954","first-page":"161","volume-title":"Correctness of pipelined machines","author":"P Manolios","year":"2000","unstructured":"Manolios P (2000) Correctness of pipelined machines. In: Formal methods in computer-aided design, FMCAD 2000, LNCS 1954. Springer, Heidelberg, pp 161\u2013178"},{"unstructured":"Manolios P, Vroon D (2003) Ordinal arithmetic in ACL2. In: ACL2 workshop 2003, Boulder, CO. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/","key":"1_CR37_1"},{"key":"1_CR38_1","series-title":"Computed aided verification, CAV \u201999, LNCS 1633","first-page":"369","volume-title":"Linking theorem proving and model-checking with well-founded bisimulation","author":"P Manolios","year":"1999","unstructured":"Manolios P, Namjoshi K, Sumners R (1999) Linking theorem proving and model-checking with well-founded bisimulation. In: Computed aided verification, CAV \u201999, LNCS 1633. Springer, Heidelberg, pp 369\u2013379"},{"doi-asserted-by":"crossref","unstructured":"Matthews J, Moore JS, Ray S, Vroon D (2006) Verification condition generation via theorem proving. In: Proceedings of 13th international conference on logic for programming, artificial intelligence, and reasoning (LPAR 2006), vol LNCS 4246, pp 362\u2013376","key":"1_CR39_1","DOI":"10.1007\/11916277_25"},{"key":"1_CR40_1","volume-title":"Piton: a mechanically verified assembly-level language","author":"JS Moore","year":"1996","unstructured":"Moore JS (1996) Piton: a mechanically verified assembly-level language. Automated reasoning series. Kluwer, Boston, MA"},{"unstructured":"Moore JS (2008) Mechanized operational semantics: lectures and supplementary material. In: Marktoberdorf summer school 2008: engineering methods and tools for software safety and security. http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/talks\/marktoberdorf-08\/index.html","key":"1_CR41_1"},{"issue":"9","key":"1_CR42_1","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"JS Moore","year":"1998","unstructured":"Moore JS, Lynch T, Kaufmann M (1998) A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. IEEE Trans Comput 47(9): 913\u2013926","journal-title":"IEEE Trans Comput"},{"issue":"3117","key":"1_CR43_1","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-3-540-27813-9_3","volume":"vol LNCS","author":"S Ray","year":"2004","unstructured":"Ray S, Hunt WA Jr (2004) Deductive verification of pipelined machines using first-order quantification. In: Proceedings of the 16th international conference on computer-aided verification (CAV 2004), vol LNCS 3117. Springer, Heidelberg, pp 31\u201343","journal-title":"Proceedings of the 16th international conference on computer-aided verification (CAV 2004)"},{"key":"1_CR44_1","first-page":"67","volume-title":"Formal methods in computer-aided design (FMCAD-2004), Lecture notes in computer science","author":"S Ray","year":"2004","unstructured":"Ray S, Moore JS (2004) Proof styles in operational semantics. In: Hu AJ, Martin AK (eds) Formal methods in computer-aided design (FMCAD-2004), Lecture notes in computer science, vol 3312. Springer, Heidelberg, pp 67\u201381"},{"issue":"4","key":"1_CR45_1","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-008-9098-1","volume":"40","author":"S Ray","year":"2008","unstructured":"Ray S, Hunt WA Jr, Matthews J, Moore JS (2008) A mechanical analysis of program verification strategies. J Autom Reason 40(4):245\u2013269","journal-title":"J Autom Reason"},{"issue":"3725","key":"1_CR46_1","first-page":"20","volume":"vol LNCS","author":"E Reeber","year":"2005","unstructured":"Reeber E, Hunt WA Jr (2005) Formalization of the DE2 language. In: Correct hardware design and verification methods (CHARME 2005), vol LNCS 3725. Springer, Heidelberg, pp 20\u201334","journal-title":"Correct hardware design and verification methods (CHARME 2005)"},{"key":"1_CR47_1","first-page":"453","volume-title":"A SAT-based decision procedure for the subclass of unrollable list functions in ACL2 (SULFA). In: Proceedings of 3rd international joint conference on automated reasoning (IJCAR 2006)","author":"E Reeber","year":"2006","unstructured":"Reeber E, Hunt WA Jr (2006) A SAT-based decision procedure for the subclass of unrollable list functions in ACL2 (SULFA). In: Proceedings of 3rd international joint conference on automated reasoning (IJCAR 2006). Springer, Heidelberg, pp 453\u2013467"},{"key":"1_CR48_1","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-1-4757-3188-0_13","volume-title":"Computer-aided reasoning: ACL2 case studies","author":"DM Russinoff","year":"2000","unstructured":"Russinoff DM, Flatau A (2000) RTL verification: a floating-point multiplier. In: Kaufmann M, Manolios P, Moore JS (eds) Computer-aided reasoning: ACL2 case studies. Kluwer, Boston, MA, pp 201\u2013232"},{"unstructured":"Russinoff D, Kaufmann M, Smith E, Sumners R (2005) Formal verification of floating-point RTL at AMD using the ACL2 theorem prover. In: IMACS\u20192005 world congress","key":"1_CR49_1"},{"key":"1_CR50_1","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-1-4757-3188-0_9","volume-title":"Computer-aided reasoning: ACL2 case studies","author":"J Sawada","year":"2000","unstructured":"Sawada J (2000) Verification of a simple pipelined machine model. In: Kaufmann M, Manolios P, Moore JS (eds) Computer-aided reasoning: ACL2 case studies. Kluwer, Boston, MA, pp 137\u2013150"},{"unstructured":"Sawada J (2002) Formal verification of divide and square root algorithms using series calculation. In: Proceedings of the ACL2 workshop, 2002, Grenoble. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2002","key":"1_CR51_1"},{"key":"1_CR52_1","first-page":"135","volume-title":"Processor verification with precise exceptions and speculative execution. In: Computer aided verification, CAV \u201998, LNCS 1427","author":"J Sawada","year":"1998","unstructured":"Sawada J, Hunt WA Jr (1998) Processor verification with precise exceptions and speculative execution. In: Computer aided verification, CAV \u201998, LNCS 1427. Springer, Heidelberg, pp 135\u2013146"},{"issue":"2","key":"1_CR53_1","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1023\/A:1014122630277","volume":"20","author":"J Sawada","year":"2002","unstructured":"Sawada J, Hunt WA Jr (2002) Verification of FM9801: an out-of-order microprocessor model with speculative execution, exceptions, and program modification capability. Formal Methods Syst Des 20(2):187\u2013222","journal-title":"Formal Methods Syst Des"},{"key":"1_CR54_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569883","volume-title":"Metamathematics, machines, and Godel\u2019s proof","author":"N Shankar","year":"1994","unstructured":"Shankar N (1994) Metamathematics, machines, and Godel\u2019s proof. Cambridge University Press, Cambridge"},{"key":"1_CR55_1","volume-title":"Mathematical logic","author":"JR Shoenfield","year":"1967","unstructured":"Shoenfield JR (1967) Mathematical logic. Addison-Wesley, Reading, MA"},{"key":"1_CR56_1","volume-title":"Common lisp the language","author":"GL Steele Jr","year":"1990","unstructured":"Steele GL Jr (1990) Common lisp the language, 2nd edn. Digital Press, Burlington, MA","edition":"2"},{"key":"1_CR57_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-aided verification \u2013 CAV \u201993","author":"M Wilding","year":"1993","unstructured":"Wilding M (1993) A mechanically verified application for a mechanically verified environment. In: Courcoubetis C (ed) Computer-aided verification \u2013 CAV \u201993, Lecture Notes in Computer Science, vol 697. Springer, Heidelberg. See ftp:\/\/ftp.cs.utexas.edu\/pub\/boyer\/nqthm\/wilding-cav93.ps"},{"key":"1_CR58_1","volume-title":"A verified code generator for a subset of Gypsy. Technical report 33","author":"WD Young","year":"1988","unstructured":"Young WD (1988) A verified code generator for a subset of Gypsy. Technical report 33. Computational Logic Inc., Austin, TX"}],"container-title":["Design and Verification of Microprocessor Systems for High-Assurance Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-1539-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,23]],"date-time":"2023-01-23T21:27:57Z","timestamp":1674509277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-1539-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781441915382","9781441915399"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_1","relation":{},"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"23 January 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}