{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:43:28Z","timestamp":1746006208721,"version":"3.40.3"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031505232"},{"type":"electronic","value":"9783031505249"}],"license":[{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-50524-9_3","type":"book-chapter","created":{"date-parts":[[2023,12,29]],"date-time":"2023-12-29T15:02:28Z","timestamp":1703862148000},"page":"50-73","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Generation of\u00a0Violation Witnesses by\u00a0Under-Approximating Abstract Interpretation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6215-7359","authenticated-orcid":false,"given":"Marco","family":"Milanese","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-3179","authenticated-orcid":false,"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,12,30]]},"reference":[{"key":"3_CR1","unstructured":"The banal static analyzer prototype. http:\/\/www.di.ens.fr\/~mine\/banal. Accessed 11 Sep 2023"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Afzal, M., et al.: Veriabs: verification by abstraction and test generation. In: 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 1138\u20131141. IEEE (2019)","DOI":"10.1109\/ASE.2019.00121"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-99253-8_2","volume-title":"Foundations of Software Science and Computation Structures","author":"F Ascari","year":"2022","unstructured":"Ascari, F., Bruni, R., Gori, R.: Limits and difficulties in the design of under-approximation abstract domains. In: FoSSaCS 2022. LNCS, vol. 13242, pp. 21\u201339. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_2"},{"issue":"5","key":"3_CR4","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1016\/j.comgeo.2009.09.002","volume":"43","author":"R Bagnara","year":"2010","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Exact join detection for convex polyhedra and other numerical abstractions. Comput. Geom. 43(5), 453\u2013473 (2010)","journal-title":"Comput. Geom."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Baldoni, R., Coppa, E., D\u2019elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. (CSUR) 51(3), 1\u201339 (2018)","DOI":"10.1145\/3182657"},{"issue":"3","key":"3_CR6","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/S0925-7721(01)00004-9","volume":"18","author":"A Bemporad","year":"2001","unstructured":"Bemporad, A., Fukuda, K., Torrisi, F.D.: Convexity recognition of the union of polyhedra. Comput. Geom. 18(3), 141\u2013154 (2001)","journal-title":"Comput. Geom."},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: Sv-comp 2023. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 495\u2013522. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 721\u2013733 (2015)","DOI":"10.1145\/2786805.2786867"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-92994-1_1","volume-title":"Tests and Proofs","author":"D Beyer","year":"2018","unstructured":"Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 3\u201323. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21, 1\u201329 (2019)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, pp. 46\u201355 (1993)","DOI":"10.1145\/155090.155095"},{"issue":"5","key":"3_CR13","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 (JACM) 50(5), 752\u2013794 (2003)","journal-title":"J. ACM (JACM)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MA Col\u00f3on","year":"2001","unstructured":"Col\u00f3on, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67\u201381. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_6"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415\u2013418. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_37"},{"key":"3_CR16","doi-asserted-by":"crossref","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 (1977)","DOI":"10.1145\/512950.512973"},{"key":"3_CR17","doi-asserted-by":"crossref","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, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"issue":"2\u20133","key":"3_CR18","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program. 13(2\u20133), 103\u2013179 (1992)","journal-title":"J. Logic Program."},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P Cousot","year":"1999","unstructured":"Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Autom. Softw. Eng. 6(1), 69\u201395 (1999)","journal-title":"Autom. Softw. Eng."},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-18275-4_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: Precondition inference from intermittent assertions and application to contracts on collections. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 150\u2013168. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_12"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-662-46681-0_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Dangl","year":"2015","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 423\u2013425. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_34"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1007\/978-3-030-72013-1_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Darke","year":"2021","unstructured":"Darke, P., Agrawal, S., Venkatesh, R.: VeriAbs: a tool for scalable verification by abstraction (competition contribution). In: TACAS 2021. LNCS, vol. 12652, pp. 458\u2013462. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_32"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-24690-6_12","volume-title":"Software Engineering and Formal Methods","author":"E de Vries","year":"2011","unstructured":"de Vries, E., Koutavas, V.: Reverse hoare logic. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 155\u2013171. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_12"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-030-32304-2_12","volume-title":"Static Analysis","author":"D Delmas","year":"2019","unstructured":"Delmas, D., Min\u00e9, A.: Analysis of software patches using numerical abstract interpretation. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 225\u2013246. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_12"},{"issue":"1\u20132","key":"3_CR26","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/S0304-3975(98)00007-3","volume":"222","author":"G Fil\u00e9","year":"1999","unstructured":"Fil\u00e9, G., Ranzato, F.: The powerset operator on abstract interpretations. Theoret. Comput. Sci. 222(1\u20132), 77\u2013111 (1999)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"3_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2651360","volume":"37","author":"G Gange","year":"2015","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. Programming Lang. Syst. (TOPLAS) 37(1), 1\u201335 (2015)","journal-title":"ACM Trans. Programming Lang. Syst. (TOPLAS)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452\u2013466. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_41"},{"key":"3_CR29","unstructured":"Gotlieb, A., Leconte, M., Marre, B.: Constraint solving on modular integers. In: ModRef Worksop, Associated to CP 2010 (2010)"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1007\/978-3-030-17184-1_26","volume-title":"Programming Languages and Systems","author":"M Journault","year":"2019","unstructured":"Journault, M., Min\u00e9, A., Ouadjaout, A.: An abstract domain for trees with numeric relations. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 724\u2013751. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_26"},{"issue":"7","key":"3_CR32","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"OOPSLA1","key":"3_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3527325","volume":"6","author":"QL Le","year":"2022","unstructured":"Le, Q.L., Raad, A., Villard, J., Berdine, J., Dreyer, D., O\u2019Hearn, P.W.: Finding real bugs in big programs with incorrectness logic. Proc. ACM Programming Lang. 6(OOPSLA1), 1\u201327 (2022)","journal-title":"Proc. ACM Programming Lang."},{"key":"3_CR34","unstructured":"Lev-Ami, T., Sagiv, M., Reps, T., Gulwani, S.: Backward analysis for inferring quantified preconditions. Tr-2007-12-01, Tel Aviv University (2007)"},{"key":"3_CR35","doi-asserted-by":"publisher","unstructured":"Marco, M., Min\u00e9, A.: Artifact of paper: Generation of Violation Witnesses by Under-Approximating Abstract Interpretation (Oct 2023). https:\/\/doi.org\/10.5281\/zenodo.8399723","DOI":"10.5281\/zenodo.8399723"},{"key":"3_CR36","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order Symbolic Comput. 19, 31\u2013100 (2006)","journal-title":"Higher-Order Symbolic Comput."},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11609773_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2005","unstructured":"Min\u00e9, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348\u2013363. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_23"},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1016\/j.scico.2013.09.014","volume":"93","author":"A Min\u00e9","year":"2014","unstructured":"Min\u00e9, A.: Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Sci. Comput. Program. 93, 154\u2013182 (2014)","journal-title":"Sci. Comput. Program."},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A., et al.: Tutorial on static inference of numeric invariants by abstract interpretation. Foundation Trends\u00ae Programming Lang. 4(3\u20134), 120\u2013372 (2017)","DOI":"10.1561\/2500000034"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78163-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y Moy","year":"2008","unstructured":"Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 188\u2013202. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_18"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. Proc. ACM Programming Lang. 4(POPL), 1\u201332 (2019)","DOI":"10.1145\/3371078"},{"key":"3_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-030-53291-8_14","volume-title":"Computer Aided Verification","author":"A Raad","year":"2020","unstructured":"Raad, A., Berdine, J., Dang, H.-H., Dreyer, D., O\u2019Hearn, P., Villard, J.: Local reasoning about the presence of bugs: incorrectness separation logic. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 225\u2013252. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_14"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1","key":"3_CR44","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.scico.2006.03.008","volume":"64","author":"DA Schmidt","year":"2007","unstructured":"Schmidt, D.A.: A calculus of logical relations for over-and underapproximating static analyses. Sci. Comput. Program. 64(1), 29\u201353 (2007)","journal-title":"Sci. Comput. Program."},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Sen, R., Srikant, Y.: Executable analysis using abstract interpretation with circular linear progressions. In: 2007 5th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2007), pp. 39\u201348. IEEE (2007)","DOI":"10.1109\/MEMCOD.2007.371251"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Simon, A., King, A.: Taming the wrapping of integer arithmetic. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 121\u2013136. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_8","DOI":"10.1007\/978-3-540-74061-2_8"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-99725-4_24","volume-title":"Static Analysis","author":"C Urban","year":"2018","unstructured":"Urban, C., Ueltschi, S., M\u00fcller, P.: Abstract interpretation of CTL properties. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 402\u2013422. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_24"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Xie, X., Chen, B., Liu, Y., Le, W., Li, X.: Proteus: computing disjunctive loop summary via path dependency analysis. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 61\u201372 (2016)","DOI":"10.1145\/2950290.2950340"}],"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-031-50524-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,7]],"date-time":"2024-11-07T02:12:32Z","timestamp":1730945552000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-50524-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,30]]},"ISBN":["9783031505232","9783031505249"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-50524-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023,12,30]]},"assertion":[{"value":"30 December 2023","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":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl24.sigplan.org\/home\/VMCAI-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"74","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}