{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T14:56:12Z","timestamp":1742396172544,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_21","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:42:14Z","timestamp":1277836934000},"page":"290-305","source":"Crossref","is-referenced-by-count":13,"title":["Approximate Symbolic Model Checking for Incomplete Designs"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nopper","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"21_CR1","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite\u2013state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"8","key":"21_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph - based algorithms for Boolean function manipulation. IEEE Trans. on Comp.\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. on Comp."},{"issue":"2","key":"21_CR3","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., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"21_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher, Dordrecht (1993)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"21_CR6","unstructured":"The VIS Group. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"21_CR7","unstructured":"McMillan, K.L.: The SMV system - for SMV version 2.5.4. Carnegie Mellon University (November 2000)"},{"key":"21_CR8","unstructured":"McMillan, K.L.: The SMV language. Cadence Berkeley Labs"},{"key":"21_CR9","unstructured":"Villa, T., Swamy, G., Shiple. VIS, T.: User\u2019s Manual. Electronics Research Laboratory, University of Colorado at Boulder"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed systems are hard to synthesize. In: In 31st IEEE Symp. Found. of Comp. Science, pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: Design Automation Conf., pp. 238\u2013243 (2001)","DOI":"10.1145\/378239.378471"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, p. 155. Springer, Heidelberg (2001)"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","first-page":"244","volume-title":"Evolutionary Programming VII","author":"K. Sajid","year":"1998","unstructured":"Sajid, K., Goel, A., Zhou, H., Aziz, A., Singhal, V.: BDD-based procedures for a theory of equality with uninterpreted functions. In Computer Aided Verification. In: Porto, V.W., Waagen, D. (eds.) EP 1998. LNCS, vol.\u00a01447, pp. 244\u2013255. Springer, Heidelberg (1998)"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Berezin, S., Biere, A., Clarke, E.M., Zhu, Y.: Combining symbolic model checking with uninterpreted functions for out-of-order processor verification. In: Int\u2019l Conf. on Formal Methods in CAD, pp. 369\u2013386 (1998)","DOI":"10.1007\/3-540-49519-3_24"},{"issue":"1","key":"21_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/371282.371364","volume":"2","author":"R.E. Bryant","year":"2001","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic\u00a02(1), 1\u201341 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Jain, A., Boppana, V., Mukherjee, R., Jain, J., Fujita, M., Hsiao, M.: Testing, verification, and diagnosis in the presence of unknowns. In: VLSI Test Symp, pp. 263\u2013269 (2000)","DOI":"10.1109\/VTEST.2000.843854"},{"key":"21_CR18","volume-title":"Digital Systems Testing and Testable Design","author":"M. Abramovici","year":"1990","unstructured":"Abramovici, M., Breuer, M.A., Friedman, A.D.: Digital Systems Testing and Testable Design. Computer Science Press, Rockville (1990)"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Scholl, C., Becker, B.: Checking equivalence for partial implementations. Technical Report 145, Albert-Ludwigs-University, Freiburg (October 2000)","DOI":"10.1007\/1-4020-2603-X_7"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Nopper, T., Scholl, C.: Symbolic model checking for incomplete designs. Technical report, Albert-Ludwigs-University, Freiburg (March 2004)","DOI":"10.1007\/978-3-540-30494-4_21"},{"key":"21_CR21","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.3.1. University of Colorado at Boulder (2001)"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Higuchi, H., Somenzi, F.: Lazy group sifting for efficient symbolic state traversal of FSMs. In: Int\u2019l Conf. on CAD, pp. 45\u201349 (1999)","DOI":"10.1109\/ICCAD.1999.810619"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Hojati, R., Krishnan, S.C., Brayton, R.K.: Early quantification and partitioned transition relations. In: Int\u2019l Conf. on Comp. Design, pp. 12\u201319 (1996)","DOI":"10.1109\/ICCD.1996.563525"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T09:56:57Z","timestamp":1740218217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}