{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:16:50Z","timestamp":1743020210022,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319395692"},{"type":"electronic","value":"9783319395708"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-39570-8_11","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T05:04:10Z","timestamp":1464066250000},"page":"158-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Configurable CEGAR Framework with Interpolation-Based Refinements"],"prefix":"10.1007","author":[{"given":"\u00c1kos","family":"Hajdu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tam\u00e1s","family":"T\u00f3th","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Istv\u00e1n","family":"Majzik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-37057-1_11","volume-title":"Fundamental Approaches to Software Engineering","author":"D Beyer","year":"2013","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varr\u00f3, D. (eds.) FASE 2013 (ETAPS 2013). LNCS, vol. 7793, pp. 146\u2013162. Springer, Heidelberg (2013)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-23404-5_3","volume-title":"Model Checking Software","author":"D Beyer","year":"2015","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Refinement selection. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 20\u201338. Springer, Heidelberg (2015)"},{"key":"11_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. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-75698-9_2","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"I Br\u00fcckner","year":"2007","unstructured":"Br\u00fcckner, I., Dr\u00e4ger, K., Finkbeiner, B., Wehrheim, H.: Slicing abstractions. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 17\u201332. Springer, Heidelberg (2007)"},{"key":"11_CR5","doi-asserted-by":"crossref","first-page":"135","DOI":"10.3233\/SAT190106","volume":"9","author":"G Cabodi","year":"2016","unstructured":"Cabodi, G., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Vendraminetto, D., Biere, A., Heljanko, K., Baumgartner, J.: Hardware model checking competition 2014: an analysis and comparison of solvers and benchmarks. J. Satisfiability Boolean Model. Comput. 9, 135\u2013172 (2016)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"issue":"5","key":"11_CR6","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"11_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"7","key":"11_CR8","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"EM Clarke","year":"2004","unstructured":"Clarke, E.M., Gupta, A., Strichman, O.: SAT-based counterexample-guided abstraction refinement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 23(7), 1113\u20131123 (2004)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"03","key":"11_CR9","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22(03), 269\u2013285 (1957)","journal-title":"J. Symbolic Logic"},{"key":"11_CR10","unstructured":"Dutertre, B., Sorea, M., et al.: Timed systems in SAL. Technical report, SRI International, Computer Science Laboratory (2004)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-642-27940-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Ermis","year":"2012","unstructured":"Ermis, E., Hoenicke, J., Podelski, A.: Splitting via interpolants. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 186\u2013201. Springer, Heidelberg (2012)"},{"issue":"6","key":"11_CR12","doi-asserted-by":"publisher","first-page":"1400","DOI":"10.1109\/TII.2015.2489184","volume":"11","author":"B Fern\u00e1ndez Adiego","year":"2015","unstructured":"Fern\u00e1ndez Adiego, B., Darvas, D., Blanco Vi\u00f1uela, E., Tournier, J.C., Bliudze, S., Blech, J.O., Gonz\u00e1lez Su\u00e1rez, V.M.: Applying model checking to industrial-sized PLC programs. IEEE Trans. Industr. Inf. 11(6), 1400\u20131410 (2015)","journal-title":"IEEE Trans. Industr. Inf."},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Formal Methods in Computer-Aided Design, pp. 1\u20138. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351148"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-39570-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,23]],"date-time":"2020-05-23T00:09:47Z","timestamp":1590192587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-39570-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319395692","9783319395708"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-39570-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"24 May 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}