{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T20:09:10Z","timestamp":1768162150564,"version":"3.49.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032159809","type":"print"},{"value":"9783032159816","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-15981-6_1","type":"book-chapter","created":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T17:13:31Z","timestamp":1768151611000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Interpretable Configuration Optimization for\u00a0Static Program Verification via\u00a0Rule-Based and\u00a0Counterfactual Reasoning"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-1756-5767","authenticated-orcid":false,"given":"Jaeseong","family":"Lee","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3594-5430","authenticated-orcid":false,"given":"Sopam","family":"Dasgupta","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9727-0362","authenticated-orcid":false,"given":"Gopal","family":"Gupta","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2826-1857","authenticated-orcid":false,"given":"Shiyi","family":"Wei","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,1,12]]},"reference":[{"key":"1_CR1","unstructured":"Titanic - machine learning from disaster (2012)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-031-57256-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2024","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS 2024. LNCS, vol. 14572, pp. 299\u2013329. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15"},{"key":"1_CR3","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":"1_CR4","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman, L.: Random forests. Mach. Learn. 45, 5\u201332 (2001)","journal-title":"Mach. Learn."},{"key":"1_CR5","unstructured":"Breiman, L., Friedman, J.H., Olshen, R.A., Stone, C.J.: Classification and regression trees. Wadsworth International Group (1984)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Chen, T., Li, M.: Multi-objectivizing software configuration tuning. In: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2021, pp. 453\u2013465. Association for Computing Machinery, New York (2021)","DOI":"10.1145\/3468264.3468555"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Cheng, J., Gao, C., Zheng, Z.: HINNPerf: hierarchical interaction neural network for performance prediction of configurable systems. ACM Trans. Softw. Eng. Methodol. 32(2) (2023)","DOI":"10.1145\/3528100"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-96145-3_10","volume-title":"Computer Aided Verification","author":"L Cordeiro","year":"2018","unstructured":"Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., Trtik, M.: JBMC: a bounded model checking tool for verifying java bytecode. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 183\u2013190. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_10"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Dasgupta, S.: Generating causally compliant counterfactual explanations using ASP. In: Proceedings 40th International Conference on Logic Programming, ICLP 2024, University of Texas at Dallas, Dallas Texas, USA, 14\u201317 October 2024. EPTCS, vol. 416, pp. 306\u2013313 (2024)","DOI":"10.4204\/EPTCS.416.30"},{"key":"1_CR10","unstructured":"Dasgupta, S., Arias, J., Salazar, E., Gupta, G.: CoGS: model agnostic causality constrained counterfactual explanations using goal-directed ASP. CoRR, abs\/2410.22615 (2024)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Dasgupta, S., Halim, S.M., Arias, J., Salazar, E., Gupta, G.: MC3G:: model agnostic causally constrained counterfactual generation. In: Gilpin, L.H., Giunchiglia, E., Hitzler, P., van Krieken, E. (eds.) Proceedings of The 19th International Conference on Neurosymbolic Learning and Reasoning. Proceedings of Machine Learning Research, vol. 284, pp. 926\u2013937. PMLR (2025)","DOI":"10.1007\/978-3-031-84924-4_14"},{"key":"1_CR12","unstructured":"Dasgupta, S., Halim, S.M., Arias, J., Salazar, E., Gupta, G.: P2C: path to counterfactuals. CoRR, abs\/2508.20371 (2025)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-031-84924-4_14","volume-title":"Practical Aspects of Declarative Languages","author":"S Dasgupta","year":"2025","unstructured":"Dasgupta, S., Shakerin, F., Arias, J., Salazar, E., Gupta, G.: C3G: causally constrained counterfactual generation. In: Erdem, E., Vidal, G. (eds.) PADL 2025. LNCS, vol. 15537, pp. 215\u2013232. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-84924-4_14"},{"key":"1_CR14","unstructured":"Dasgupta, S., Shakerin, F., Salazar, E., Arias, J., Gupta, G.: Causally constrained counterfactual generation using ASP. In: Workshop Proceedings of the 40th International Conference on Logic Programming (ICLP-WS 2024) co-located with the 40th International Conference on Logic Programming (ICLP 2024), Dallas, TX, USA, 12th\u20133th October 2024. CEUR Workshop Proceedings, vol. 3799. CEUR-WS.org (2024)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Dorn, J., Apel, S., Siegmund, N.: Mastering uncertainty in performance estimations of configurable software systems. In: Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2020, pp. age 684\u2013696. Association for Computing Machinery, New York (2021)","DOI":"10.1145\/3324884.3416620"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Gelfond, M., Kahl, Y.: Knowledge Representation, Reasoning, and the Design of Intelligent Agents: Answer Set Programming Approach. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781139342124"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Guo, J., Czarnecki, K., Apely, S., Siegmundy, N., Wasowski, A.: Variability-aware performance prediction: a statistical learning approach. In: Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2013, pp. 301\u2013311. IEEE Press (2013)","DOI":"10.1109\/ASE.2013.6693089"},{"issue":"3","key":"1_CR18","doi-asserted-by":"publisher","first-page":"1826","DOI":"10.1007\/s10664-017-9573-6","volume":"23","author":"J Guo","year":"2018","unstructured":"Guo, J., et al.: Data-efficient performance learning for configurable systems. Empir. Softw. Eng. 23(3), 1826\u20131867 (2018)","journal-title":"Empir. Softw. Eng."},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Ha, H., Zhang, H.: DeepPerf: performance prediction for configurable software with deep sparse neural network. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE), pp. 1095\u20131106 (2019)","DOI":"10.1109\/ICSE.2019.00113"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Humphreys, J., Dam, H.K.: An explainable deep model for defect prediction. In: Proceedings of the 7th International Workshop on Realizing Artificial Intelligence Synergies in Software Engineering, RAISE 2019, pp. 49\u201355. IEEE Press (2019)","DOI":"10.1109\/RAISE.2019.00016"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Jiarpakdee, J., Tantithamthavorn, C.K., Grundy, J.C.: Practitioners\u2019 perceptions of the goals and visual explanations of defect prediction models. In: 2021 IEEE\/ACM 18th International Conference on Mining Software Repositories (MSR), pp. 432\u2013443 (2021)","DOI":"10.1109\/MSR52588.2021.00055"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-319-41528-4_19","volume-title":"Computer Aided Verification","author":"T Kahsai","year":"2016","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Koc, U., Mordahl, A, Wei, S., Foster, J.S., Porter, A.A.: Satune: a study-driven auto-tuning approach for configurable software verification tools. In: 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 330\u2013342 (2021)","DOI":"10.1109\/ASE51524.2021.9678761"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Lhot\u00e1k, O., Hendren, L.: Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation. ACM Trans. Softw. Eng. Methodol. 18(1) (2008)","DOI":"10.1145\/1391984.1391987"},{"key":"1_CR26","unstructured":"Lundberg, S.M., Lee, S.-I.: A unified approach to interpreting model predictions. In: Proceedings of the 31st International Conference on Neural Information Processing Systems, NIPS 2017, pp. 4768\u20134777. Curran Associates Inc., Red Hook (2017)"},{"key":"1_CR27","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809071","volume-title":"Introduction to Information Retrieval","author":"CD Manning","year":"2008","unstructured":"Manning, C.D., Raghavan, P., Sch\u00fctze, H.: Introduction to Information Retrieval. Cambridge University Press, Cambridge (2008)"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Nair, V., Menzies, T., Siegmund, N., Apel, S.: Using bad learners to find good configurations. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2017, pp. 257\u2013267. Association for Computing Machinery, New York (2017)","DOI":"10.1145\/3106237.3106238"},{"issue":"7","key":"1_CR29","doi-asserted-by":"publisher","first-page":"794","DOI":"10.1109\/TSE.2018.2870895","volume":"46","author":"V Nair","year":"2020","unstructured":"Nair, V., Yu, Z., Menzies, T., Siegmund, N., Apel, S.: Finding faster configurations using flash. IEEE Trans. Softw. Eng. 46(7), 794\u2013811 (2020)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Oh, J., Batory, D., Myers, M., Siegmund, N.: Finding near-optimal configurations in product lines by random sampling. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2017, pp. 61\u201371. Association for Computing Machinery, New York (2017)","DOI":"10.1145\/3106237.3106273"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Pornprasit, C., Tantithamthavorn, C.K.: Jitline: a simpler, better, faster, finer-grained just-in-time defect prediction. In: 2021 IEEE\/ACM 18th International Conference on Mining Software Repositories (MSR), pp. 369\u2013379 (2021)","DOI":"10.1109\/MSR52588.2021.00049"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Ribeiro, M.T., Singh, S., Guestrin, C.: \u201cWhy should i trust you?\": explaining the predictions of any classifier. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD 2016, pp. 1135\u20131144. Association for Computing Machinery, New York (2016)","DOI":"10.1145\/2939672.2939778"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Sarkar, A., Guo, J., Siegmund, N., Apel, S., Czarnecki, K.: Cost-efficient sampling for performance prediction of configurable systems (t). In: 2015 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 342\u2013352 (2015)","DOI":"10.1109\/ASE.2015.45"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Shu, Y., Sui, Y., Zhang, H., Xu, G.: Perf-AL: performance prediction for configurable software through adversarial learning. In: Proceedings of the 14th ACM\/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM), ESEM 2020. Association for Computing Machinery, New York (2020)","DOI":"10.1145\/3382494.3410677"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Siegmund, N., Grebhahn, A., Apel, S., K\u00e4stner, C.: Performance-influence models for highly configurable systems. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2015, pp. 284\u2013294. Association for Computing Machinery, New York (2015)","DOI":"10.1145\/2786805.2786845"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-32469-7_14","volume-title":"Formal Methods for Industrial Critical Systems","author":"J Slab\u00fd","year":"2012","unstructured":"Slab\u00fd, J., Strej\u010dek, J., Trt\u00edk, M.: Checking properties described by state machines: on synergy of instrumentation, slicing, and symbolic execution. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 207\u2013221. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32469-7_14"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"630","DOI":"10.1007\/978-3-642-36742-7_50","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Slaby","year":"2013","unstructured":"Slaby, J., Strej\u010dek, J., Trt\u00edk, M.: Symbiotic: synergy of instrumentation, slicing, and symbolic execution. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 630\u2013632. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_50"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Smaragdakis, Y., Bravenboer, M., Lhot\u00e1k, O.: Pick your contexts well: understanding object-sensitivity. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 17\u201330. Association for Computing Machinery, New York (2011)","DOI":"10.1145\/1926385.1926390"},{"issue":"11","key":"1_CR39","doi-asserted-by":"publisher","first-page":"1200","DOI":"10.1109\/TSE.2018.2876537","volume":"46","author":"C Tantithamthavorn","year":"2020","unstructured":"Tantithamthavorn, C., Hassan, A.E., Matsumoto, K.: The impact of class rebalancing techniques on the performance and interpretation of defect prediction models. IEEE Trans. Softw. Eng. 46(11), 1200\u20131219 (2020)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-031-52038-9_3","volume-title":"Practical Aspects of Declarative Languages","author":"H Wang","year":"2024","unstructured":"Wang, H., Gupta, G.: FOLD-SE: an efficient rule-based machine learning algorithm with scalable explainability. In: Gebser, M., Sergey, I. (eds.) PADL 2024. LNCS, vol. 14512, pp. 37\u201353. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-52038-9_3"},{"key":"1_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1007\/978-3-319-89884-1_23","volume-title":"Programming Languages and Systems","author":"S Wei","year":"2018","unstructured":"Wei, S., Mardziel, P., Ruef, A., Foster, J.S., Hicks, M.: Evaluating design tradeoffs in numeric static analysis for java. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 653\u2013682. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_23"},{"issue":"1","key":"1_CR42","first-page":"565","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Int. Res. 32(1), 565\u2013606 (2008)","journal-title":"J. Artif. Int. Res."},{"issue":"3","key":"1_CR43","doi-asserted-by":"publisher","first-page":"539","DOI":"10.14778\/3632093.3632114","volume":"17","author":"X Zhang","year":"2023","unstructured":"Zhang, X., et al.: An efficient transfer learning based configuration adviser for database tuning. Proc. VLDB Endow. 17(3), 539\u2013552 (2023)","journal-title":"Proc. VLDB Endow."},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Zheng, W., Shen, T., Chen, X., Deng, P.: Interpretability application of the just-in-time software defect prediction model. J. Syst. Softw. 188(C) (2022)","DOI":"10.1016\/j.jss.2022.111245"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15981-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T17:13:34Z","timestamp":1768151614000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15981-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032159809","9783032159816"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15981-6_1","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":"12 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PADL","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Practical Aspects of Declarative Languages","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":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"padl2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl26.sigplan.org\/home\/PADL-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}