{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:44Z","timestamp":1725511904623},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540712084"},{"type":"electronic","value":"9783540712091"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_31","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"405-419","source":"Crossref","is-referenced-by-count":7,"title":["Combining Abstraction Refinement and SAT-Based Model Checking"],"prefix":"10.1007","author":[{"given":"Nina","family":"Amla","sequence":"first","affiliation":[]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","first-page":"254","volume-title":"Correct Hardware Design and Verification Methods","author":"R.P. Kurshan","year":"2005","unstructured":"Kurshan, R.P., et al.: An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 254\u2013268. Springer, Heidelberg (2005)"},{"key":"31_CR2","series-title":"Lecture Notes in Computer Science","first-page":"260","volume-title":"Formal Methods in Computer-Aided Design","author":"K.L. McMillan","year":"2004","unstructured":"McMillan, K.L., Amla, N.: 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":"31_CR3","series-title":"Lecture Notes in Computer Science","first-page":"230","volume-title":"Formal Methods in Computer-Aided Design","author":"F. Somenzi","year":"2004","unstructured":"Somenzi, F., Awedh, M.: Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 230\u2013244. Springer, Heidelberg (2004)"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science\u00a066(2) (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., et al.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"31_CR6","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":"31_CR7","unstructured":"Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. In: LICS (1990)"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Improving SAT-based bounded model checking by means of bdd-based approximate traversals. In: DATE (2003)","DOI":"10.1109\/DATE.2003.1253720"},{"key":"31_CR9","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logics of Programs (1981)"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: DATE (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Gupta, A., et al.: Learning from BDDs in SAT-based bounded model checking. In: DAC (2003)","DOI":"10.1145\/775832.776040"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"Gupta, A., et al.: Iterative abstraction using SAT-based BMC with proof analysis. In: ICCAD (2003)","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"31_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/11513988_11","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2005","unstructured":"Gupta, A., Strichman, O.: Abstraction Refinement for Bounded Model Checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 112\u2013124. Springer, Heidelberg (2005)"},{"key":"31_CR15","unstructured":"Huang, C.Y., et al.: Static property checking using atpg versus bdd techniques. In: ITC (2000)"},{"key":"31_CR16","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":"31_CR17","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. In: Formal Methods in System Design (2001)","DOI":"10.1006\/inco.2000.2893"},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","first-page":"227","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Somenzi","year":"2006","unstructured":"Somenzi, F., Li, B.: Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 227\u2013241. Springer, Heidelberg (2006)"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Li, B., Wang, C., Somenzi, F.: Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. In: STTT (2005)","DOI":"10.1007\/s10009-004-0169-2"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/11560548_33","volume-title":"Correct Hardware Design and Verification Methods","author":"J. Marques-Silva","year":"2005","unstructured":"Marques-Silva, J.: Improvements to the Implementation of Interpolant-Based Model Checking. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 367\u2013370. Springer, Heidelberg (2005)"},{"key":"31_CR21","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":"31_CR22","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: 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":"31_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic Abstraction without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., et al.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"31_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":"31_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":"31_CR27","series-title":"Lecture Notes in Computer Science","first-page":"31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Somenzi","year":"2004","unstructured":"Somenzi, F., Ravi, K.: Minimal Assignments for Bounded Model Checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 31\u201345. Springer, Heidelberg (2004)"},{"key":"31_CR28","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","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T21:21:07Z","timestamp":1683926467000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_31","relation":{},"subject":[]}}