{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T21:06:56Z","timestamp":1772831216457,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540291053","type":"print"},{"value":"9783540320302","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_19","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"238-253","source":"Crossref","is-referenced-by-count":13,"title":["A New SAT-Based Algorithm for Symbolic Trajectory Evaluation"],"prefix":"10.1007","author":[{"given":"Jan-Willem","family":"Roorda","sequence":"first","affiliation":[]},{"given":"Koen","family":"Claessen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Aagaard, M., Jones, R.B., Melham, T.F., O\u2019Leary, J.W., Seger, C.-J.H.: A methodology for large-scale hardware verification. In: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (2000)","DOI":"10.1007\/3-540-40922-X_17"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"Computer Aided Verification","author":"P. Bjesse","year":"2001","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 454. Springer, Heidelberg (2001)"},{"key":"19_CR4","unstructured":"http:\/\/www.intel.com\/software\/products\/opensource\/tools1\/verification"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. In: 34th Design Automation Conference (DAC 1997), pp. 167\u2013172. Association for Computing Machinery (1997)","DOI":"10.1109\/DAC.1997.597138"},{"key":"19_CR6","first-page":"1","volume-title":"Proceedings of the 40th conference on Design automation","author":"T. Schubert","year":"2003","unstructured":"Schubert, T.: High level formal verification of next-generation microprocessors. In: Proceedings of the 40th conference on Design automation, pp. 1\u20136. ACM Press, New York (2003)"},{"issue":"2","key":"19_CR7","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design: An International Journal\u00a06(2), 147\u2013189 (1995)","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"19_CR9","unstructured":"Yang, J., Gil, R., Singerman, E.: SatGSTE: Combining the abstraction of GSTE with the capacity of a SAT solver. In: Designing Correct Circuits (DCC 2004) (2004)"},{"key":"19_CR10","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1109\/ICCD.2001.955052","volume-title":"IEEE International Conference on Computer Design: VLSI in Computers & Processors (ICCD 2001)","author":"J. Yang","year":"2001","unstructured":"Yang, J., Seger, C.-J.H.: Introduction to generalized symbolic trajectory evaluation. In: IEEE International Conference on Computer Design: VLSI in Computers & Processors (ICCD 2001), Washington - Brussels - Tokyo, September 2001, pp. 360\u2013367. IEEE, Los Alamitos (2001)"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:13:09Z","timestamp":1619507589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/11560548_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}