{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T05:27:50Z","timestamp":1725600470465},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226847"},{"type":"electronic","value":"9783642226854"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22685-4_36","type":"book-chapter","created":{"date-parts":[[2011,8,10]],"date-time":"2011-08-10T08:54:39Z","timestamp":1312966479000},"page":"402-413","source":"Crossref","is-referenced-by-count":2,"title":["Making Abstraction-Refinement Efficient in Model Checking"],"prefix":"10.1007","author":[{"given":"Cong","family":"Tian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"36_CR1","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.: Desigh and syntesis of of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131. Springer, Heidelberg (1982)"},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th International Symposium on Programming, pp. 337\u2013350 (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"36_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample guided abstraction refinement. In: Emerson, E., Sistla, A. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"36_CR4","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S.A. Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math.\u00a09, 67\u201396 (1963)","journal-title":"Z. Math. Logik Grund. Math."},{"issue":"7","key":"36_CR5","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Gupta, A., Strichman, O.: SAT Based Counterexample-Guided Abstraction-Refinement. IEEE Trans. Computer Aided Design\u00a023(7), 1113\u20131123 (2004)","journal-title":"IEEE Trans. Computer Aided Design"},{"issue":"1","key":"36_CR6","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TC.2009.105","volume":"59","author":"F. He","year":"2010","unstructured":"He, F., Song, X., Hung, W.N.N., Gu, M., Sun, J.: Integrating Evolutionary Computation with Abstraction Refinement for Model Checking. IEEE Trans. Computers\u00a059(1), 116\u2013126 (2010)","journal-title":"IEEE Trans. Computers"},{"key":"36_CR7","unstructured":"Rushby, J.: Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem proving. Presented at Theoretical and Practical Aspects of SPIN Model Checking: Proc. 5th and 6th Int. SPIN Workshops, citeseer.nj.nec.com\/rushby99integrated.html"},{"issue":"3","key":"36_CR8","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1093\/comjnl\/bxm085","volume":"52","author":"F. He","year":"2009","unstructured":"He, F., Song, X., Gu, M., Sun, J.-G.: Heuristic-Guided Abstraction Refinement. Comput. J.\u00a052(3), 280\u2013287 (2009)","journal-title":"Comput. J."},{"issue":"1","key":"36_CR9","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TC.2009.105","volume":"59","author":"F. He","year":"2010","unstructured":"He, F., Song, X., Hung, W.N.N., Gu, M., Sun, J.: Integrating Evolutionary Computation with Abstraction Refinement for Model Checking. IEEE Trans. Computers\u00a059(1), 116\u2013126 (2010)","journal-title":"IEEE Trans. Computers"},{"key":"36_CR10","volume-title":"Computer Aided Verificaton of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer Aided Verificaton of Coordinating Processes. Princeton Univ. Press, Princeton (1994)"},{"issue":"11","key":"36_CR11","doi-asserted-by":"publisher","first-page":"2297","DOI":"10.1109\/TCAD.2006.873897","volume":"25","author":"C. Wang","year":"2006","unstructured":"Wang, C., Li, B., Jin, H., Hachtel, G.D., Somenzi, F.: Improving Ariadne\u2019s Bundle by Following Multiple Threads in Abstraction Refinement. IEEE Trans. Computer Aided Design\u00a025(11), 2297\u20132316 (2006)","journal-title":"IEEE Trans. Computer Aided Design"},{"key":"36_CR12","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.H., Strichman, O.: SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 265\u2013279. Springer, Heidelberg (2002)"},{"key":"36_CR13","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.M., 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":"36_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proc. Symp. Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"36_CR15","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.: Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 176\u2013191. Springer, Heidelberg (2003)"},{"key":"36_CR16","doi-asserted-by":"crossref","unstructured":"Govindaraju, S.G., Dill, D.L.: Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking. In: Proc. Int\u2019l Conf. Computer-Aided Design (ICCAD), pp. 115\u2013119 (2000)","DOI":"10.21236\/ADA401014"}],"container-title":["Lecture Notes in Computer Science","Computing and Combinatorics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22685-4_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T03:49:04Z","timestamp":1638244144000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22685-4_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226847","9783642226854"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22685-4_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}