{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:37:46Z","timestamp":1743043066761,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":15,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9780387307701"},{"type":"electronic","value":"9780387301624"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-0-387-30162-4_416","type":"book-chapter","created":{"date-parts":[[2008,6,26]],"date-time":"2008-06-26T18:30:58Z","timestamp":1214505058000},"page":"932-935","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Amit","family":"Prakash","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"416_CR1_416","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic Model Checking Using Sat Procedures Instead of BDDs. In: ACM Design Automation Conference. (1999)","DOI":"10.21236\/ADA360973"},{"key":"416_CR2_416","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Trans. Comp. C-35, 677\u2013691 (1986)","journal-title":"IEEE Trans. Comp."},{"issue":"2","key":"416_CR3_416","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Symbolic Model Checking: 1020 States and Beyond. Inf. Comp. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comp."},{"key":"416_CR4_416","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.H., Stein, C.: Introduction to Algorithms. MIT Press (2001)","edition":"2"},{"key":"416_CR5_416","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Formal Models and Semantics, vol. B of Handbook of Theoretical Computer Science, pp.\u00a0996\u20131072. Elsevier Science (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"416_CR6_416","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF00121125","volume":"1","author":"A. Gupta","year":"1993","unstructured":"Gupta, A.: Formal Hardware Verification Methods: A\u00a0Survey. Formal Method Syst. Des. 1, 151\u2013238 (1993)","journal-title":"Formal Method Syst. Des."},{"key":"416_CR7_416","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2006)"},{"key":"416_CR8_416","unstructured":"Katz, R.: Contemporary logic design. Benjamin\/Cummings Pub. Co. (1993)"},{"key":"416_CR9_416","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"416_CR10_416","doi-asserted-by":"crossref","unstructured":"Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R., Kuehlmann, A.: Scalable Automated Verification via Expert-System Guided Transformations. In: Formal Methods in CAD. (2004)","DOI":"10.1007\/978-3-540-30494-4_12"},{"key":"416_CR11_416","unstructured":"Ranjan, R., Aziz, A., Brayton, R., Plessier, B., Pixley, C.: Efficient BDD Algorithms for FSM Synthesis and Verification. In: Proceedings of the International Workshop on Logic Synthesis, May 1995"},{"key":"416_CR12_416","unstructured":"Savoj, H.: Don't Cares in Multi-Level Network Optimization. Ph.\u202fD. thesis, University of California, Berkeley, Electronics Research Laboratory, College of Engineering. University of California, Berkeley, CA (1992)"},{"key":"416_CR13_416","doi-asserted-by":"crossref","unstructured":"Shiple, T.R., Hojati, R., Sangiovanni-Vincentelli, A.L., Brayton, R.K.: Heuristic Minimization of BDDs Using Don't Cares. In: ACM Design Automation Conference, San Diego, CA, June (1994)","DOI":"10.1145\/196244.196360"},{"key":"416_CR14_416","doi-asserted-by":"crossref","unstructured":"Touati, H., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Implicit State Enumeration of Finite State Machines using BDDs. In: IEEE International Conference on Computer-Aided Design, pp.\u00a0130\u2013133, November (1990)","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"416_CR15_416","unstructured":"Wile, B., Goss, J., Roesner, W.: Comprehensive Functional Verification. Morgan-Kaufmann (2005)"}],"container-title":["Encyclopedia of Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-30162-4_416","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T21:32:20Z","timestamp":1738272740000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-0-387-30162-4_416"}},"subtitle":["1990; Burch, Clarke, McMillan, Dill"],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9780387307701","9780387301624"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-30162-4_416","relation":{},"subject":[],"published":{"date-parts":[[2008]]}}}