{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T13:35:02Z","timestamp":1762954502744},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"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":[[2005]]},"DOI":"10.1007\/11560548_20","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T05:38:22Z","timestamp":1128577102000},"page":"254-268","source":"Crossref","is-referenced-by-count":45,"title":["An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment"],"prefix":"10.1007","author":[{"given":"Nina","family":"Amla","sequence":"first","affiliation":[]},{"given":"Xiaoqun","family":"Du","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Kuehlmann","sequence":"additional","affiliation":[]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-36577-X_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Amla","year":"2003","unstructured":"Amla, N., Kurshan, R., McMillan, K., Medel, R.: Experimental analysis of different techniques for bounded model checking. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 34\u201348. Springer, Heidelberg (2003)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-30494-4_19","volume-title":"Formal Methods in Computer-Aided Design","author":"N. Amla","year":"2004","unstructured":"Amla, N., McMillan, K.: A hybrid of counterexample-based and proof-based abstraction. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 260\u2013274. Springer, Heidelberg (2004)"},{"key":"20_CR3","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, p. 193. Springer, Heidelberg (1999)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulations. IEEE Transactions on Computers (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"20_CR5","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. In: LICS (1990)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_3","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Chauhan","year":"2002","unstructured":"Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131. Springer, Heidelberg (1982)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F. Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 436. Springer, Heidelberg (2001)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Formal Models and Sematics, vol.\u00a0B (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"20_CR10","unstructured":"Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: ICCAD (2004)"},{"key":"20_CR11","unstructured":"Goldberg, E., Novikov, Y.: Berkmin: A fast and robust sat-solver. In: DATE (2002)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Iyer, M., Parthasarathy, G., Cheng, K.T.: SATORI- an efficient sequential SAT solver for circuits. In: ICCAD (2003)","DOI":"10.1109\/ICCAD.2003.159706"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11527695_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"H. Jin","year":"2005","unstructured":"Jin, H., Somenzi, F.: CirCUs: Hybrid satisfiability solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 211\u2013223. Springer, Heidelberg (2005)"},{"key":"20_CR14","unstructured":"Kuehlmann, A.: Dynamic transition relation simplification for bounded property checking. In: ICCAD (2004)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. In: TCAD (2003)","DOI":"10.1109\/TCAD.2002.804386"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. Formal Methods in System Design (2001)","DOI":"10.1006\/inco.2000.2893"},{"key":"20_CR17","volume-title":"Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R. Kurshan","year":"1994","unstructured":"Kurshan, R.: Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Li, B., Wang, C., Somenzi, F.: A satisfiability-based approach to abstraction refinement in model checking. In: Workshop on BMC (2003)","DOI":"10.1016\/S1571-0661(05)82546-0"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: A search algorithm for propositional satisfiability. IEEETC: IEEE Transactions on Computers\u00a048 (1999)","DOI":"10.1109\/12.769433"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"2003","unstructured":"McMillan, K.: Applying SAT methods in unbounded symbolic model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725. Springer, Heidelberg (2003)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"2003","unstructured":"McMillan, K.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. McMillan","year":"2003","unstructured":"McMillan, K., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"20_CR24","unstructured":"Parthasarathy, G., Iyer, M., Cheng, K.T., Wang, L.C.: A comparison of BDDs, BMC, and sequential SAT for model checking. In: High-Level Design Validation and Test Workshop (2003)"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in sat-based formal verification. In: STTT (2005)","DOI":"10.1007\/s10009-004-0183-4"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proc. of the 5th International Symposium on Programming (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"20_CR28","unstructured":"Wang, C., Li, B., Jin, H., Hachtel, G., Somenzi, F.: Improving ariadne\u2019s bundle by following multiple threads in abstraction refinement. In: ICCAD (2003)"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.: Satire: A new incremental satisfiability engine. In: DAC (2001)","DOI":"10.1145\/378239.379019"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T20:13:07Z","timestamp":1683231187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/11560548_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}