{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:56:47Z","timestamp":1779087407568,"version":"3.51.4"},"publisher-location":"Cham","reference-count":103,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_13","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"385-419","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Abstraction and Abstraction Refinement"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Dams","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"13_CR1","first-page":"170","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: uncertainty, but with precision. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0170\u2013179. ACM, New York (2004)"},{"key":"13_CR2","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-30494-4_19","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"N. Amla","year":"2004","unstructured":"Amla, N., McMillan, K.L.: A hybrid of counterexample-based and proof-based abstraction. In: Hu, A.J., Martin, A.K. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol.\u00a03312, pp.\u00a0260\u2013274. Springer, Heidelberg (2004)"},{"key":"13_CR3","series-title":"LNCS","first-page":"268","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02031, pp.\u00a0268\u2013283. Springer, Heidelberg (2001)"},{"key":"13_CR4","unstructured":"Ball, T., Rajamani, S.: Boolean programs: a model and process for software analysis. Tech. Rep. 2000-14, Microsoft Research (2000)"},{"key":"13_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a0260\u2013264. Springer, Heidelberg (2001)"},{"key":"13_CR6","series-title":"LNCS","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Barner","year":"2002","unstructured":"Barner, S., Geist, D., Gringauze, A.: Symbolic localization reduction with reconstruction layering and backtracking. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS. Springer, Heidelberg (2002)"},{"key":"13_CR7","series-title":"LNCS","first-page":"2","volume-title":"SAS","author":"D. Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A., Henzinger, T.A., Jhala, R., Majumdar, R.: The BLAST query language for software verification. In: Giacobazzi, R. (ed.) SAS. LNCS, vol.\u00a03148, pp.\u00a02\u201318. Springer, Heidelberg (2004)"},{"key":"13_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04590, pp.\u00a0504\u2013518. Springer, Heidelberg (2007)"},{"key":"13_CR9","first-page":"29","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"D. Beyer","year":"2008","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a029\u201338. IEEE, Piscataway (2008)"},{"key":"13_CR10","volume-title":"Handbook of Model Checking","author":"A. Biere","year":"2018","unstructured":"Biere, A., Kroening, D.: SAT-based model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"13_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-70545-1_14","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"M.G. Bobaru","year":"2008","unstructured":"Bobaru, M.G., Pasareanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05123, pp.\u00a0135\u2013148. Springer, Heidelberg (2008)"},{"key":"13_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0023733","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Bouajjani","year":"1990","unstructured":"Bouajjani, A., Fernandez, J., Halbwachs, N.: Minimal model generation. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0531, pp.\u00a0197\u2013203. Springer, Heidelberg (1990)"},{"key":"13_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-56496-9_9","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Bouali","year":"1992","unstructured":"Bouali, A., de Simone, R.: Symbolic bisimulation minimisation. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0663, pp.\u00a096\u2013108. Springer, Heidelberg (1992)"},{"key":"13_CR14","volume-title":"Handbook of Model Checking","author":"J. Bradfield","year":"2018","unstructured":"Bradfield, J., Walukiewicz, I.: The mu-calculus and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"issue":"1\u20132","key":"13_CR15","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1\u20132), 115\u2013131 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"G. Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, pp.\u00a0274\u2013287. Springer, Heidelberg (1999)"},{"key":"13_CR17","series-title":"LNCS","first-page":"168","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"G. Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01877, pp.\u00a0168\u2013182. Springer, Heidelberg (2000)"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-27836-8_26","volume-title":"Intl. Colloquium on Automata, Languages, and Programming (ICALP)","author":"G. Bruns","year":"2004","unstructured":"Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: Intl. Colloquium on Automata, Languages, and Programming (ICALP), pp.\u00a0281\u2013293. Springer, Heidelberg (2004)"},{"key":"13_CR19","first-page":"397","volume-title":"Design Automation Conf. (DAC)","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E., Beatty, D.L., Seger, C.J.H.: Formal hardware verification by symbolic ternary trajectory evaluation. In: Design Automation Conf. (DAC), pp.\u00a0397\u2013402 (1991)"},{"issue":"2","key":"13_CR20","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/635499.635502","volume":"4","author":"D. Bustan","year":"2003","unstructured":"Bustan, D., Grumberg, O.: Simulation-based minimization. ACM Trans. Comput. Log. 4(2), 181\u2013206 (2003)","journal-title":"ACM Trans. Comput. Log."},{"key":"13_CR21","volume-title":"Handbook of Model Checking","author":"S. Chaki","year":"2018","unstructured":"Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"13_CR22","series-title":"LNCS","first-page":"276","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Chaki","year":"2007","unstructured":"Chaki, S., Strichman, O.: Optimized L*-based assume-guarantee reasoning. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, pp.\u00a0276\u2013291. Springer, Heidelberg (2007)"},{"key":"13_CR23","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","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: Formal Methods in Computer Aided Design (FMCAD). IEEE, Piscataway (2002)"},{"key":"13_CR24","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M. Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12, 371\u2013408 (2003)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"13_CR25","unstructured":"Chechik, M., Devereux, B., Gurfinkel, A., Easterbrook, S.: Multi-valued symbolic model-checking. Tech. Rep. CSRG-448, University of Toronto (2002)"},{"key":"13_CR26","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"Y. Chen","year":"2007","unstructured":"Chen, Y., He, Y., Xie, F., Yang, J.: Automatic abstraction refinement for generalized symbolic trajectory evaluation. In: Formal Methods in Computer Aided Design (FMCAD). IEEE\/ACM, Piscataway\/New York (2007)"},{"key":"13_CR27","series-title":"LNCS","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"H. Chockler","year":"2008","unstructured":"Chockler, H., Grumberg, O., Yadgar, A.: Efficient automatic STE refinement using responsibility. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04963. Springer, Heidelberg (2008)"},{"key":"13_CR28","series-title":"LNCS","first-page":"310","volume-title":"CAV","author":"A. Cimatti","year":"2011","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos\u2014a software model checker for SystemC. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol.\u00a06806, pp.\u00a0310\u2013316. Springer, Heidelberg (2011)"},{"issue":"5","key":"13_CR29","doi-asserted-by":"publisher","first-page":"774","DOI":"10.1109\/TCAD.2012.2232351","volume":"32","author":"A. Cimatti","year":"2013","unstructured":"Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking SystemC. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 32(5), 774\u2013787 (2013)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"issue":"5","key":"13_CR30","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. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"13_CR31","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR32","series-title":"LNCS","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"E. Clarke","year":"2002","unstructured":"Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02404. Springer, Heidelberg (2002)"},{"key":"13_CR33","series-title":"LNCS","first-page":"570","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a03440, pp.\u00a0570\u2013574. Springer, Heidelberg (2005)"},{"issue":"5","key":"13_CR34","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR35","first-page":"19","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"E.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Symp. on Logic in Computer Science (LICS), pp.\u00a019\u201329. IEEE, Piscataway (2002)"},{"issue":"2\u20133","key":"13_CR36","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Form. Methods Syst. Des. 25(2\u20133), 105\u2013127 (2004)","journal-title":"Form. Methods Syst. Des."},{"key":"13_CR37","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1145\/234528.234740","volume":"28","author":"P. Cousot","year":"1996","unstructured":"Cousot, P.: Abstract interpretation. ACM Comput. Surv. 28, 324\u2013328 (1996)","journal-title":"ACM Comput. Surv."},{"key":"13_CR38","first-page":"238","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0238\u2013252. ACM, New York (1977)"},{"key":"13_CR39","first-page":"12","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"2000","unstructured":"Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a012\u201325. ACM, New York (2000)"},{"issue":"2","key":"13_CR40","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. Trans. Program. Lang. Syst. 19(2), 253\u2013291 (1997)","journal-title":"Trans. Program. Lang. Syst."},{"key":"13_CR41","first-page":"335","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"D. Dams","year":"2004","unstructured":"Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0335\u2013344. IEEE, Piscataway (2004)"},{"key":"13_CR42","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-30579-8_15","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"D. Dams","year":"2005","unstructured":"Dams, D., Namjoshi, K.S.: Automata as abstractions. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a03385, pp.\u00a0216\u2013232. Springer, Heidelberg (2005)"},{"issue":"2","key":"13_CR43","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/BF00264365","volume":"24","author":"R. Nicola De","year":"1987","unstructured":"De Nicola, R.: Extensional equivalences for transition systems. Acta Inform. 24(2), 211\u2013237 (1987)","journal-title":"Acta Inform."},{"issue":"2","key":"13_CR44","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995)","journal-title":"J. ACM"},{"key":"13_CR45","series-title":"EPTCS","first-page":"49","volume-title":"Proc. Combined 19th Intl. Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, EXPRESS\/SOS","author":"M. Gazda","year":"2012","unstructured":"Gazda, M., Willemse, T.A.C.: Expressiveness and completeness in abstraction. In: Luttik, B., Reniers, M.A. (eds.) Proc. Combined 19th Intl. Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, EXPRESS\/SOS. EPTCS, vol.\u00a089, pp.\u00a049\u201364 (2012)"},{"key":"13_CR46","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45657-0_11","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02404, pp.\u00a0137\u2013150. Springer, Heidelberg (2002)"},{"key":"13_CR47","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01254, pp.\u00a072\u201383. Springer, Heidelberg (1997)"},{"key":"13_CR48","series-title":"LNCS","volume-title":"Intl. Conf. on Formal Methods for Components and Objects (FMCO)","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O.: Abstraction and refinement in model checking. In: Intl. Conf. on Formal Methods for Components and Objects (FMCO). LNCS, vol.\u00a04111. Springer, Heidelberg (2005)"},{"key":"13_CR49","series-title":"LNCS","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Lange, M., Leucker, M., Shoham, S.: Don\u2019t know in \u03bc$\\mu$-calculus. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS. Springer, Heidelberg (2005)"},{"key":"13_CR50","doi-asserted-by":"publisher","first-page":"1130","DOI":"10.1016\/j.ic.2006.10.009","volume":"205","author":"O. Grumberg","year":"2007","unstructured":"Grumberg, O., Lange, M., Leucker, M., Shoham, S.: When not losing is better than winning: abstraction and refinement for the full mu-calculus. Inf. Comput. 205, 1130\u20131148 (2007)","journal-title":"Inf. Comput."},{"key":"13_CR51","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16, 843\u2013872 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR52","series-title":"LNCS","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"O. Grumberg","year":"2007","unstructured":"Grumberg, O., Schuster, A., Yadgar, A.: 3-valued circuit SAT for STE with automatic refinement. In: Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a04762. Springer, Heidelberg (2007)"},{"key":"13_CR53","first-page":"416","volume-title":"International Conference on Computer Aided Design (ICCAD)","author":"A. Gupta","year":"2003","unstructured":"Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative abstraction using SAT-based BMC with proof analysis. In: International Conference on Computer Aided Design (ICCAD), p.\u00a0416. IEEE, Piscataway (2003)"},{"key":"13_CR54","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11513988_11","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Gupta","year":"2005","unstructured":"Gupta, A., Strichman, O.: Abstraction refinement for bounded model checking. In: Etessami, K., Rajamani, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03576, pp.\u00a0112\u2013124. Springer, Heidelberg (2005)"},{"key":"13_CR55","series-title":"LNCS","first-page":"212","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Chechik, M.: Why waste a perfectly good abstraction? In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, pp.\u00a0212\u2013226. Springer, Heidelberg (2006)"},{"issue":"1","key":"13_CR56","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"key":"13_CR57","first-page":"453","volume-title":"FOCS: Foundations of Computer Science","author":"M.R. Henzinger","year":"1995","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: FOCS: Foundations of Computer Science, pp.\u00a0453\u2013462. IEEE, Piscataway (1995)"},{"key":"13_CR58","first-page":"232","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0232\u2013244. ACM, New York (2004)"},{"key":"13_CR59","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"POPL","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) POPL, pp.\u00a0232\u2013244. ACM, New York (2004)"},{"key":"13_CR60","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"T.A. Henzinger","year":"2002","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 (POPL), pp.\u00a058\u201370. ACM, New York (2002)"},{"key":"13_CR61","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) Programming Languages and Systems. LNCS, vol.\u00a02028, pp.\u00a0155\u2013169. Springer, Heidelberg (2001)"},{"key":"13_CR62","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/11817963_15","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"H. Jain","year":"2006","unstructured":"Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0137\u2013151. Springer, Heidelberg (2006)"},{"key":"13_CR63","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1109\/TCAD.2007.907270","volume":"27","author":"H. Jain","year":"2008","unstructured":"Jain, H., Kroening, D., Sharygina, N., Clarke, E.: Word level predicate abstraction and refinement for verifying RTL Verilog. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 27, 366\u2013379 (2008)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"13_CR64","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04590, pp.\u00a0193\u2013206. Springer, Heidelberg (2007)"},{"key":"13_CR65","volume-title":"Handbook of Model Checking","author":"R. Jhala","year":"2018","unstructured":"Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"issue":"1","key":"13_CR66","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Inf. Comput. 163(1), 203\u2013243 (2000)","journal-title":"Inf. Comput."},{"key":"13_CR67","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/BFb0012782","volume-title":"9th Colloquium on Automata, Languages and Programming (ICALP)","author":"D. Kozen","year":"1982","unstructured":"Kozen, D.: Results on the propositional \u03bc$\\mu$-calculus. In: 9th Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0140, pp.\u00a0348\u2013359. Springer, Heidelberg (1982)"},{"key":"13_CR68","first-page":"1325","volume-title":"Design, Automation & Test in Europe (DATE)","author":"D. Kroening","year":"2007","unstructured":"Kroening, D., Sharygina, N.: Image computation and predicate refinement for RTL Verilog using word level proofs. In: Lauwereins, R., Madsen, J. (eds.) Design, Automation & Test in Europe (DATE), pp.\u00a01325\u20131330. ACM, New York (2007)"},{"key":"13_CR69","series-title":"LNCS","first-page":"573","volume-title":"CAV","author":"D. Kroening","year":"2011","unstructured":"Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol.\u00a06806, pp.\u00a0573\u2013578. Springer, Heidelberg (2011)"},{"key":"13_CR70","series-title":"Princeton Series in Computer Science","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton Series in Computer Science. Princeton University Press, Princeton (1994)"},{"key":"13_CR71","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. Log. Methods Comput. Sci. 3(2) (2007)","DOI":"10.2168\/LMCS-3(2:1)2007"},{"key":"13_CR72","first-page":"203","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"K. Larsen","year":"1988","unstructured":"Larsen, K., Thomsen, B.: A modal process logic. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0203\u2013210. IEEE, Piscataway (1988)"},{"key":"13_CR73","first-page":"108","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0108\u2013117. IEEE, Piscataway (1990)"},{"key":"13_CR74","first-page":"264","volume-title":"Proceedings of the 24th Annual ACM Symposium on Theory of Computing","author":"D. Lee","year":"1992","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems (extended abstract). In: Proceedings of the 24th Annual ACM Symposium on Theory of Computing, pp.\u00a0264\u2013274. ACM, New York (1992)"},{"issue":"2","key":"13_CR75","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10009-004-0169-2","volume":"7","author":"B. Li","year":"2005","unstructured":"Li, B., Wang, C., Somenzi, F.: Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. Int. J. Softw. Tools Technol. Transf. 7(2), 143\u2013155 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR76","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Form. Methods Syst. Des. 6, 11\u201345 (1995)","journal-title":"Form. Methods Syst. Des."},{"issue":"5","key":"13_CR77","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1134\/S0361768812050039","volume":"38","author":"M. Mandrykin","year":"2012","unstructured":"Mandrykin, M., Mutilin, V., Novikov, E., Khoroshilov, A.V., Shved, P.: Using Linux device drivers for static verification tools benchmarking. Program. Comput. Softw. 38(5), 245\u2013256 (2012)","journal-title":"Program. Comput. Softw."},{"key":"13_CR78","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0123\u2013136. Springer, Heidelberg (2006)"},{"key":"13_CR79","series-title":"LNCS","first-page":"2","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02619, pp.\u00a02\u201317. Springer, Heidelberg (2003)"},{"key":"13_CR80","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-04761-9_21","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"Y. Meller","year":"2009","unstructured":"Meller, Y., Grumberg, O., Shoham, S.: A framework for compositional verification of multi-valued systems via abstraction-refinement. In: Liu, Z., Ravn, A.P. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a05799, pp.\u00a0271\u2013288. Springer, Heidelberg (2009)"},{"key":"13_CR81","first-page":"481","volume-title":"Intl. Joint Conf. on Artificial Intelligence (IJCAI)","author":"R. Milner","year":"1971","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Intl. Joint Conf. on Artificial Intelligence (IJCAI), pp.\u00a0481\u2013489. British Computer Society, London (1971)"},{"key":"13_CR82","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-45069-6_29","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K. Namjoshi","year":"2003","unstructured":"Namjoshi, K.: Abstraction for branching time properties. In: Hunt, W.A., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02725, pp.\u00a0288\u2013300. Springer, Heidelberg (2003)"},{"key":"13_CR83","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"5th GI-Conference on Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: 5th GI-Conference on Theoretical Computer Science. LNCS, vol.\u00a0104, pp.\u00a0167\u2013183. Springer, Heidelberg (1981)"},{"key":"13_CR84","volume-title":"Handbook of Model Checking","author":"N. Piterman","year":"2018","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"13_CR85","first-page":"105","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"M. Sagiv","year":"1999","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0105\u2013118. ACM, New York (1999)"},{"key":"13_CR86","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-540-45099-3_20","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"H. Sa\u00efdi","year":"2000","unstructured":"Sa\u00efdi, H.: Model checking guided abstraction and analysis. In: Palsberg, J. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a01824, pp.\u00a0377\u2013396. Springer, Heidelberg (2000)"},{"key":"13_CR87","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"H. Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01633, pp.\u00a0443\u2013454. Springer, Heidelberg (1999)"},{"key":"13_CR88","volume-title":"Handbook of Model Checking","author":"S.A. Seshia","year":"2018","unstructured":"Seshia, S.A., Sharygina, N., Tripakis, S.: Modeling for verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"issue":"1","key":"13_CR89","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-011-0185-y","volume":"14","author":"N. Sharygina","year":"2012","unstructured":"Sharygina, N., Tonetta, S., Tsitovich, A.: An abstraction refinement approach combining precise and approximated techniques. Int. J. Softw. Tools Technol. Transf. 14(1), 1\u201314 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR90","series-title":"LNCS","first-page":"331","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Shoham","year":"2004","unstructured":"Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02988, pp.\u00a0331\u2013346 (2004)"},{"key":"13_CR91","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/11562948_27","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"S. Shoham","year":"2005","unstructured":"Shoham, S., Grumberg, O.: Multi-valued model checking games. In: Peled, D.A., Tsay, Y.K. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a03707, pp.\u00a0354\u2013369. Springer, Heidelberg (2005)"},{"key":"13_CR92","series-title":"LNCS","volume-title":"SAS\u201907","author":"S. Shoham","year":"2007","unstructured":"Shoham, S., Grumberg, O.: Compositional verification and 3-valued abstractions join forces. In: SAS\u201907. LNCS, vol.\u00a04634. Springer, Heidelberg (2007)"},{"issue":"1","key":"13_CR93","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1297658.1297659","volume":"9","author":"Sharon Shoham","year":"2007","unstructured":"Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Transactions on Computer Logic (TOCL) 9 (2007)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"11","key":"13_CR94","doi-asserted-by":"publisher","first-page":"1313","DOI":"10.1016\/j.ic.2008.07.004","volume":"206","author":"S. Shoham","year":"2008","unstructured":"Shoham, S., Grumberg, O.: 3-valued abstraction: more precision at less cost. Inf. Comput. 206(11), 1313\u20131333 (2008)","journal-title":"Inf. Comput."},{"key":"13_CR95","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-14295-6_45","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Singh","year":"2010","unstructured":"Singh, R., Giannakopoulou, D., Pasareanu, C.: Learning component interfaces with may and must abstractions. In: Touili, T., Cook, B., Jackson, P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06174, pp.\u00a0527\u2013542. Springer, Heidelberg (2010)"},{"key":"13_CR96","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3550-5","volume-title":"Modal and Temporal Properties of Processes","author":"C. Stirling","year":"2001","unstructured":"Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, Heidelberg (2001)"},{"key":"13_CR97","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/11817963_20","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Tzoref","year":"2006","unstructured":"Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0190\u2013204 (2006)"},{"key":"13_CR98","unstructured":"Uribe, T.: Abstraction-based deductive-algorithmic verification of reactive systems. Ph.D. thesis, Computer Science Department, Stanford University (1998). Technical report STAN-CS-TR-99-1618"},{"key":"13_CR99","first-page":"173","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"Y. Vizel","year":"2012","unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Lazy abstraction and SAT-based reachability in hardware model checking. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0173\u2013181. IEEE, Piscataway (2012)"},{"key":"13_CR100","first-page":"210","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"B. Wachter","year":"2013","unstructured":"Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0210\u2013217. IEEE, Piscataway (2013)"},{"key":"13_CR101","unstructured":"Wikipedia: The free encyclopedia. www.wikipedia.org (2011). Accessed 15 Nov. 2015"},{"key":"13_CR102","first-page":"501","volume-title":"Intl. Conf. on Automated Software Engineering (ASE), ASE \u201907","author":"T. Witkowski","year":"2007","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: Intl. Conf. on Automated Software Engineering (ASE), ASE \u201907, pp.\u00a0501\u2013504. ACM, New York (2007)"},{"key":"13_CR103","unstructured":"Yahav, E., Reps, T., Sagiv, M.: LTL model checking for systems with unbounded number of dynamically created threads and objects. Tech. Rep. TR-1424, Computer Sciences Department, University of Wisconsin, Madison, WI (2001)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T21:58:20Z","timestamp":1661291900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":103,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_13","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}