{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T10:37:38Z","timestamp":1768214258912,"version":"3.49.0"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-15700-3_12","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:22:04Z","timestamp":1768202524000},"page":"237-262","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Input-Based Three-Valued Abstraction Refinement"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2069-8584","authenticated-orcid":false,"given":"Jan","family":"Onderka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1710-1513","authenticated-orcid":false,"given":"Stefan","family":"Ratschan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274\u2013287. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_25","DOI":"10.1007\/3-540-48683-6_25"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Bruns, G., Godefroid, P.: Generalized Model Checking: Reasoning about Partial State Spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168\u2013182. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44618-4_14","DOI":"10.1007\/3-540-44618-4_14"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Bruns, G., Godefroid, P.: Temporal logic query checking. In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pp. 409\u2013417. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932516","DOI":"10.1109\/LICS.2001.932516"},{"issue":"2","key":"12_CR4","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/103516.103519","volume":"38","author":"RE Bryant","year":"1991","unstructured":"Bryant, R.E.: A methodology for hardware verification based on logic simulation. J. ACM 38(2), 299\u2013328 (1991). https:\/\/doi.org\/10.1145\/103516.103519","journal-title":"J. ACM"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Bryant, R.E., Seger, C.-J.H.: Formal verification of digital circuits using symbolic ternary system models. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 33\u201343. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023717","DOI":"10.1007\/BFb0023717"},{"issue":"1","key":"12_CR6","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1109\/43.62795","volume":"10","author":"R Bryant","year":"1991","unstructured":"Bryant, R.: Formal verification of memory circuits by switch-level simulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 10(1), 94\u2013102 (1991). https:\/\/doi.org\/10.1109\/43.62795","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Chen, Y., He, Y., Xie, F., Yang, J.: Automatic abstraction refinement for generalized symbolic trajectory evaluation. In: Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings, IEEE Comput. Soc. 111\u2013118 (2007). https:\/\/doi.org\/10.1109\/FAMCAD.2007.11","DOI":"10.1109\/FAMCAD.2007.11"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"issue":"5","key":"12_CR9","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM 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). https:\/\/doi.org\/10.1145\/186025.186051","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"12_CR10","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Gupta, A., Strichman, O.: SAT-based counterexample-guided abstraction refinement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 23(7), 1113\u20131123 (2004). https:\/\/doi.org\/10.1109\/TCAD.2004.829807","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. POPL \u201977, Association for Computing Machinery, New York, NY, USA (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1979, p. 269\u2013282. Association for Computing Machinery, New York, NY, USA (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Cranen, S., Groote, J.F., Reniers, M.A.: A linear translation from CTL* to the first-order modal $$\\upmu $$-calculus. Theor. Comput. Sci. 412(28), 3129\u20133139 (2011). https:\/\/doi.org\/10.1016\/J.TCS.2011.02.034","DOI":"10.1016\/J.TCS.2011.02.034"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Dam, M.: Fixed points of B\u00fcchi automata. In: Shyamasundar, R. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 39\u201350. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-56287-7_93","DOI":"10.1007\/3-540-56287-7_93"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Dams, D., Grumberg, O.: Abstraction and Abstraction Refinement. In: FSTTCS 1992. LNCS, vol. 652, pp. 385\u2013419. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_13","DOI":"10.1007\/978-3-319-10575-8_13"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Interval analysis and machine arithmetic: Why signedness ignorance is bliss. ACM Trans. Program. Lang. Syst. 37(1),(2015). https:\/\/doi.org\/10.1145\/2651360","DOI":"10.1145\/2651360"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"49","DOI":"10.4204\/eptcs.89.5","volume":"89","author":"M Gazda","year":"2012","unstructured":"Gazda, M., Willemse, T.A.: Expressiveness and completeness in abstraction. Electr. Proc. Theor. Comput. Sci. 89, 49\u201364 (2012). https:\/\/doi.org\/10.4204\/eptcs.89.5","journal-title":"Electr. Proc. Theor. Comput. Sci."},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: May\/must abstraction-based software model checking for sound verification and falsification. In: Grumberg, O., Seidl, H., Irlbeck, M. (eds.) Software Systems Safety, NATO Science for Peace and Security Series, D: Information and Communication Security, vol.\u00a036, pp. 1\u201316. IOS Press (2014). https:\/\/doi.org\/10.3233\/978-1-61499-385-8-1","DOI":"10.3233\/978-1-61499-385-8-1"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-Based Model Checking Using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426\u2013440. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44685-0_29","DOI":"10.1007\/3-540-44685-0_29"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Jagadeesan, R.: Automatic Abstraction Using Generalized Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 137\u2013151. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_11","DOI":"10.1007\/3-540-45657-0_11"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Jagadeesan, R.: On the Expressiveness of 3-Valued Models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 206\u2013222. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36384-X_18","DOI":"10.1007\/3-540-36384-X_18"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Grumberg, O., Lange, M., Leucker, M., Shoham, S.: Don\u2019t Know in the $$\\upmu $$-Calculus. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 233\u2013249. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_16","DOI":"10.1007\/978-3-540-30579-8_16"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Grumberg, O., Lange, M., Leucker, M., Shoham, S.: When not losing is better than winning: Abstraction and refinement for the full $$\\upmu $$-calculus. Inf. Comput. 205(8), 1130\u20131148 (2007). https:\/\/doi.org\/10.1016\/j.ic.2006.10.009","DOI":"10.1016\/j.ic.2006.10.009"},{"key":"12_CR24","unstructured":"G\u00fcckel, D.: Synthesis of State Space Generators for Model Checking Microcontroller Code. Dissertation thesis, RWTH Aachen (2014). http:\/\/aib.informatik.rwth-aachen.de\/2014\/2014-15.pdf"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"G\u00fcckel, D., Kowalewski, S.: Automatic Derivation of Abstract Semantics From Instruction Set Descriptions. In: Brauer, J., Roveri, M., Tews, H. (eds.) 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), vol.\u00a024, pp. 71\u201383. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2012). https:\/\/doi.org\/10.4230\/OASIcs.SSV.2011.71","DOI":"10.4230\/OASIcs.SSV.2011.71"},{"key":"12_CR26","unstructured":"Gurfinkel, A.: Yasm: Software model-checker. https:\/\/www.cs.toronto.edu\/~arie\/yasm\/"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-45187-7_18","volume-title":"CONCUR 2003 - Concurrency Theory","author":"A Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M.: Multi-valued model checking via classical model checking. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 266\u2013280. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45187-7_18"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/11691372_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Chechik, M.: Why waste a perfectly good abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 212\u2013226. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_14"},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11817963_18","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Yasm: A software model-checker for verification and refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 170\u2013174. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_18"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-88387-6_9","volume-title":"Automated Technology for Verification and Analysis","author":"A Gurfinkel","year":"2008","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Model checking recursive programs with exact predicate abstraction. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 95\u2013110. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88387-6_9"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-45694-5_16","volume-title":"CONCUR 2002 \u2014 Concurrency Theory","author":"B Konikowska","year":"2002","unstructured":"Konikowska, B., Penczek, W.: Reducing model checking from multi-valued CTL* to CTL*. In: Brim, L., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A., Jan\u010dar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 226\u2013239. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45694-5_16"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1007\/978-3-319-10575-8_25","volume-title":"CONCUR 2002 \u2014 Concurrency Theory","author":"T Melham","year":"2018","unstructured":"Melham, T.: Symbolic trajectory evaluation. In: CONCUR 2002. LNCS, vol. 2421, pp. 831\u2013870. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_25"},{"key":"12_CR33","unstructured":"Microchip Technology Inc.: ATmega48A\/PA\/88A\/PA\/168A\/PA\/328\/P Data Sheet (2018). http:\/\/ww1.microchip.com\/downloads\/en\/DeviceDoc\/ATmega48A-PA-88A-PA-168A-PA-328-P-DS-DS40002061A.pdf. dS40002061A"},{"key":"12_CR34","unstructured":"Microchip Technology Inc.: AVR Instruction Set Manual (2021). https:\/\/ww1.microchip.com\/downloads\/en\/DeviceDoc\/AVR-InstructionSet-Manual-DS40002198.pdf. dS40002198B"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"Nelson, L., Bornholt, J., Gu, R., Baumann, A., Torlak, E., Wang, X.: Scaling symbolic evaluation for automated verification of systems code with Serval. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles, pp. 225\u2013242. SOSP \u201919, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3341301.3359641","DOI":"10.1145\/3341301.3359641"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Noll, T., Schlich, B.: Delayed nondeterminism in model checking embedded systems assembly code. In: Yorav, K. (ed.) Hardware and Software: Verification and Testing, pp. 185\u2013201. Springer, Berlin Heidelberg, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-77966-7_16","DOI":"10.1007\/978-3-540-77966-7_16"},{"key":"12_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-540-77966-7_16","volume-title":"Hardware and Software: Verification and Testing","author":"T Noll","year":"2008","unstructured":"Noll, T., Schlich, B.: Delayed nondeterminism in model checking embedded systems assembly code. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 185\u2013201. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-77966-7_16"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Onderka, J.: Formal verification of machine-code systems by translation of simulable descriptions. In: Proceedings of the 13th Mediterranean Conference on Embedded Computing, MECO 2024, pp.\u00a01\u20134 (2024). https:\/\/doi.org\/10.1109\/MECO62516.2024.10577942","DOI":"10.1109\/MECO62516.2024.10577942"},{"key":"12_CR39","unstructured":"Onderka, J.: Abstraction-Based Machine-Code Program Verification. Doctoral thesis, Czech Technical University in Prague (2025). http:\/\/hdl.handle.net\/10467\/122640"},{"key":"12_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-030-94583-1_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Onderka","year":"2022","unstructured":"Onderka, J., Ratschan, S.: Fast three-valued abstract bit-vector arithmetic. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 242\u2013262. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_12"},{"key":"12_CR41","doi-asserted-by":"publisher","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, pp. 27\u201373. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_2","DOI":"10.1007\/978-3-319-10575-8_2"},{"key":"12_CR42","doi-asserted-by":"publisher","unstructured":"Reinbacher, T., Brauer, J., Horauer, M., Schlich, B.: Refining assembly code static analysis for the Intel MCS-51 microcontroller. In: Proceedings of the Fourth IEEE International Symposium on Industrial Embedded Systems, SIES 2009, pp. 161\u2013170 (2009). https:\/\/doi.org\/10.1109\/SIES.2009.5196212","DOI":"10.1109\/SIES.2009.5196212"},{"key":"12_CR43","unstructured":"Rigorous Engineering of Mainstream Systems Project: Islaris: verification of machine code against authoritative ISA semantics (2023). https:\/\/github.com\/rems-project\/islaris"},{"key":"12_CR44","doi-asserted-by":"publisher","unstructured":"Sammler, M., et al.: In: Islaris: Verification of Machine Code Against Authoritative ISA Semantics, pp. 825\u2013840. , ACM, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523434","DOI":"10.1145\/3519939.3523434"},{"key":"12_CR45","doi-asserted-by":"publisher","unstructured":"Schlich, B., Kowalewski, S.: [mc]square: A model checker for microcontroller code. In: Proceedings of the Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISOLA 2006, pp. 466\u2013473 (2006). https:\/\/doi.org\/10.1109\/ISoLA.2006.62","DOI":"10.1109\/ISoLA.2006.62"},{"key":"12_CR46","doi-asserted-by":"crossref","unstructured":"Schlich, B.: Model checking of software for microcontrollers. ACM Trans. Embedded Comput. Syst. 9(4) (2010). https:\/\/doi.org\/10\/bm83n7","DOI":"10.1145\/1721695.1721702"},{"key":"12_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-45069-6_28","volume-title":"Computer Aided Verification","author":"S Shoham","year":"2003","unstructured":"Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275\u2013287. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_28"},{"key":"12_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-24730-2_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Shoham","year":"2004","unstructured":"Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546\u2013560. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_40"},{"issue":"11","key":"12_CR49","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). https:\/\/doi.org\/10.1016\/j.ic.2008.07.004","journal-title":"Inf. Comput."},{"key":"12_CR50","unstructured":"The UNSAT group: Serval (2019). https:\/\/unsat.cs.washington.edu\/projects\/serval\/"},{"key":"12_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/11817963_20","volume-title":"Computer Aided Verification","author":"R Tzoref","year":"2006","unstructured":"Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 190\u2013204. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_20"},{"issue":"1","key":"12_CR52","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.ic.2010.08.001","volume":"209","author":"O Wei","year":"2011","unstructured":"Wei, O., Gurfinkel, A., Chechik, M.: On the consistency, expressiveness, and precision of partial modeling formalisms. Inf. Comput. 209(1), 20\u201347 (2011). https:\/\/doi.org\/10.1016\/j.ic.2010.08.001","journal-title":"Inf. Comput."},{"key":"12_CR53","doi-asserted-by":"publisher","unstructured":"Yang, J., Seger, C.J.: Introduction to generalized symbolic trajectory evaluation. In: Proceedings 2001 IEEE International Conference on Computer Design: VLSI in Computers and Processors. ICCD 2001, pp. 360\u2013365 (2001). https:\/\/doi.org\/10.1109\/ICCD.2001.955052","DOI":"10.1109\/ICCD.2001.955052"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:22:07Z","timestamp":1768202527000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}