{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:10:27Z","timestamp":1761621027564},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_44","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T14:39:50Z","timestamp":1265899190000},"page":"454-464","source":"Crossref","is-referenced-by-count":47,"title":["Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers"],"prefix":"10.1007","author":[{"given":"Per","family":"Bjesse","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Leonard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abdel","family":"Mokkedem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"44_CR1","doi-asserted-by":"crossref","unstructured":"M. Aagaard, R.B. Jones, T.F. Melham, J.W. O\u2019Leary, and C.-J. H. Seger. A methodology for large-scale hardware verification. In Formal Methods in Computer Aided Design, November 2000.","DOI":"10.1007\/3-540-40922-X_17"},{"key":"44_CR2","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, P. Bjesse, and N. E\u00e9n. Symbolic reachability analysis based on SAT-solvers. In Proc. TACAS\u2019 00, 9 th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2000.","DOI":"10.1007\/3-540-46419-0_28"},{"key":"44_CR3","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS\u2019 99, 8 th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 1999.","DOI":"10.21236\/ADA360973"},{"key":"44_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, E.M. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC[tm] microprocessor using symbolic model checking without BDDs. In Proc. 11 th Int. Conf. on Computer Aided Verification, 1999.","DOI":"10.1007\/3-540-48683-6_8"},{"key":"44_CR5","doi-asserted-by":"crossref","unstructured":"P. Bjesse and K. Claessen. SAT-based verification without state space traversal. In Formal Methods in Computer Aided Design, November 2000.","DOI":"10.1007\/3-540-40922-X_23"},{"key":"44_CR6","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, December 1999."},{"key":"44_CR7","doi-asserted-by":"crossref","unstructured":"A. Gupta, Z. Yang, and P. Ashar. SAT-based image computation with application in reachability analysis for verification. In Formal Methods in Computer Aided Design, November 2000.","DOI":"10.1007\/3-540-40922-X_22"},{"issue":"1\/2","key":"44_CR8","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"C.N. Ip and D. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1\/2):41\u201375, August 1996.","journal-title":"Formal Methods in System Design"},{"key":"44_CR9","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"44_CR10","unstructured":"K.L. McMillan. The SMV language. Technical report, Cadence Berkeley Labs, 1999."},{"key":"44_CR11","unstructured":"Prover Technology AB. Prover 4.0 Application Programming Reference Manual, 2000. PPI-01-ARM-1."},{"issue":"2","key":"44_CR12","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J. H. Seger","year":"1995","unstructured":"C.-J. H. Seger and R.E. Bryant. Formal verification by symbolic evaluation of partially ordered trajectories. Formal Methods in System Design, 6(2):147\u2013190, March 1995.","journal-title":"Formal Methods in System Design"},{"key":"44_CR13","doi-asserted-by":"crossref","unstructured":"M. Sheeran, S. Singh, and G. St\u00e4lmarck. Checking safety properties using induction and a SAT-solver. In Formal Methods in Computer Aided Design, November 2000.","DOI":"10.1007\/3-540-40922-X_8"},{"issue":"1","key":"44_CR14","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M. Sheeran","year":"2000","unstructured":"M. Sheeran and G. St\u00e4lmarck. A tutorial on St\u00e4lmarck\u2019s proof procedure for propositional logic. Formal Methods in System Design, 16(1):23\u201358, January 2000.","journal-title":"Formal Methods in System Design"},{"key":"44_CR15","unstructured":"J.P.M. Silva. Search algorithms for satisfiability problems in combinational switching circuits. PhD thesis, EECS Department, University of Michigan, May 1995."},{"key":"44_CR16","doi-asserted-by":"crossref","unstructured":"P.F. Williams, A. Biere, E.M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Proc. 12th Int. Conf. on Computer Aided Verification, 2000.","DOI":"10.1007\/10722167_13"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T18:29:45Z","timestamp":1558808985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_44","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}