{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:55:10Z","timestamp":1725551710853},"publisher-location":"Berlin, Heidelberg","reference-count":17,"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_19","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T14:42:14Z","timestamp":1277822534000},"page":"260-274","source":"Crossref","is-referenced-by-count":16,"title":["A Hybrid of Counterexample-Based and Proof-Based Abstraction"],"prefix":"10.1007","author":[{"given":"Nina","family":"Amla","sequence":"first","affiliation":[]},{"given":"Ken L.","family":"McMillan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/3-540-56922-7_4","volume-title":"Computer Aided Verification","author":"F. Balarin","year":"1993","unstructured":"Balarin, F., Sangiovanni-Vincentelli, A.: An iterative approach to language containment. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 29\u201340. Springer, Heidelberg (1993)"},{"key":"19_CR2","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. In: LICS (June 1990)"},{"key":"19_CR3","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":"19_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45657-0_20","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Gupta, A., Kukula, J., Strichman, O.: SAT based abstractionrefinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 265. Springer, Heidelberg (2002)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-36577-X_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Glusman","year":"2003","unstructured":"Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiplecounterexample guided iterative abstraction refinement. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 176\u2013191. Springer, Heidelberg (2003)"},{"key":"19_CR7","unstructured":"Govindaraju, S.G., Dill, D.L.: Counterexample-Guided choice of projections in approximate symbolic model checking. In: ICCAD (2000)"},{"key":"19_CR8","unstructured":"Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative abstraction using sat-based bmc with proof analysis. In: ICCAD (2003)"},{"issue":"3","key":"19_CR9","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design\u00a019(3), 291\u2013314 (2001)","journal-title":"Formal Methods in System Design"},{"key":"19_CR10","volume-title":"Computer-Aided-Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided-Verification of Coordinating Processes. Princeton University Press, Princeton (1994)"},{"key":"19_CR11","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.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F.,, Y.Z.L.Z., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Lichtenstein, O.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL (1985)","DOI":"10.1145\/318593.318622"},{"key":"19_CR14","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP\u2013a new search algorithm for satisfiability. In: ICCAD (1996)"},{"key":"19_CR15","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Logic in Computer Science (LICS 1986), pp. 322\u2013331 (1986)"},{"key":"19_CR16","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":"19_CR17","doi-asserted-by":"crossref","unstructured":"Wang, D., Ho, P., Long, J., Kukula, J.H., Zhu, Y., Tony Ma, H., Damiano, R.: Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In: Design Automation Conference, pp. 35\u201340 (2001)","DOI":"10.1145\/378239.378260"}],"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_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:25:26Z","timestamp":1558279526000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}