{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:19:06Z","timestamp":1742390346583,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_38","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"453-467","source":"Crossref","is-referenced-by-count":6,"title":["A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)"],"prefix":"10.1007","author":[{"given":"Erik","family":"Reeber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"38_CR1","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)","journal-title":"London Mathematical Society Journal of Computation and Mathematics"},{"key":"38_CR2","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1145\/378239.379017","volume-title":"Proceedings of the 38th Design Automation Conference (DAC 2001)","author":"M. Moskewicz","year":"2001","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535. ACM, New York (2001)"},{"key":"38_CR3","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 Publishers, Dordrecht (2000)"},{"issue":"2","key":"38_CR4","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast Decision Procedures Based on Congruence Closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Seminars in Mathematics 8 (1968)","key":"38_CR5"},{"doi-asserted-by":"crossref","unstructured":"Sankaralingam, K., Nagarajan, R., Liu, H., Kim, C., Huh, J., Burger, D., Keckler, S., Moore, C.: exploiting ilp, tlp, and dlp with the polymorphous trips architecture. In: International Symposium on Computer Architecture, pp. 422\u2013433 (2003)","key":"38_CR6","DOI":"10.1145\/871656.859667"},{"doi-asserted-by":"crossref","unstructured":"Sethumadhavan, S., Desikan, R., Burger, D., Moore, C.R., Keckler, S.W.: Scalable Hardware Memory Disambiguation for High ILP Processors. In: Proceedings of the 36th Annual International Symposium on Microarchitecture (MICRO 36), pp. 399\u2013410. ACM\/IEEE (2003)","key":"38_CR7","DOI":"10.1109\/MICRO.2003.1253244"},{"key":"38_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11560548_5","volume-title":"Correct Hardware Design and Verification Methods","author":"J..W.A. Hunt","year":"2005","unstructured":"Hunt, J.W.A., Reeber, E.: Formalization of the DE2 Language. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 20\u201334. Springer, Heidelberg (2005)"},{"key":"38_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining Specification, Proof Checking, and Model Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"issue":"4","key":"38_CR10","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1109\/54.936245","volume":"18","author":"R.B. Jones","year":"2001","unstructured":"Jones, R.B., O\u2019Leary, J.W., Seger, C.J.H., Aagaard, M., Melham, T.F.: Practical Formal Verification in Microprocessor Design. IEEE Design & Test of Computers\u00a018(4), 16\u201325 (2001)","journal-title":"IEEE Design & Test of Computers"},{"unstructured":"Berezin, S.: Model Checking and Theorem Proving: A Unified Framework. PhD thesis, Carnegie Mellon University (2002)","key":"38_CR11"},{"issue":"1","key":"38_CR12","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BF00881842","volume":"12","author":"J. Moore","year":"1994","unstructured":"Moore, J.: Introduction to the OBDD Algorithm for the ATP Community. Journal of Automated Reasoning\u00a012(1), 33\u201345 (1994)","journal-title":"Journal of Automated Reasoning"},{"unstructured":"Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, The University of Texas at Austin (2001)","key":"38_CR13"},{"doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.K.: Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements. In: DATE, pp. 168\u2013175 (2004)","key":"38_CR14","DOI":"10.1109\/DATE.2004.1268844"},{"key":"38_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-45069-6_33","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E.: Deductive Verification of Advanced Out-of-Order Microprocessors. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 341\u2013353. Springer, Heidelberg (2003)"},{"unstructured":"The SAT-extended ACL2 Theorem Prover (2006), www.cs.utexas.edu\/users\/reeber\/sat-extended-acl2.html","key":"38_CR16"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T06:09:22Z","timestamp":1736575762000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11814771_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}