{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T14:35:11Z","timestamp":1742999711191,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308192"},{"type":"electronic","value":"9783031308208"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show how to generate a constraint system of symbolic expressions as part of an inter-procedural constraint-system\u2013based program analysis such that any chosen slice of the intended analysis may be computed through the evaluation of the symbolic constraints. Thus, our method ensures that the computed expressions provide genuine explanations for the chosen analysis slice. The resulting system is then annotated with program location information, translated into closed-form expressions, and simplified to yield a human-readable justification for the analyzer\u2019s verdict. Justifications are given using program locations, constants from the program, abstract lattice operations, loops in the analysis, and computed results.\n<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_27","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"453-472","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis"],"prefix":"10.1007","author":[{"given":"Kalmer","family":"Apinis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vesal","family":"Vojdani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"27_CR1","doi-asserted-by":"publisher","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.: Abstraction-carrying code. In: Logic for Programming, Artificial Intelligence, and Reasoning, pp. 380\u2013397, Springer (2005), https:\/\/doi.org\/10.1007\/978-3-540-32275-7_25","DOI":"10.1007\/978-3-540-32275-7_25"},{"key":"27_CR2","doi-asserted-by":"publisher","unstructured":"Amato, G., Scozzari, F., Seidl, H., Apinis, K., Vojdani, V.: Efficiently intertwining widening and narrowing. Science of Computer Programming 120, 1\u201324 (2016), https:\/\/doi.org\/10.1016\/j.scico.2015.12.005","DOI":"10.1016\/j.scico.2015.12.005"},{"key":"27_CR3","doi-asserted-by":"publisher","unstructured":"Amtoft, T.: Partial Evaluation for Constraint-Based Program Analyses. Tech. rep., BRICS Report Series RS-99-45, Department of Computer Science, University of Aarhus (1999), https:\/\/doi.org\/10.7146\/brics.v6i45.20115","DOI":"10.7146\/brics.v6i45.20115"},{"key":"27_CR4","doi-asserted-by":"publisher","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: How to combine widening and narrowing for non-monotonic systems of equations. ACM SIGPLAN Notices 48(6), 377\u2013386 (2013), https:\/\/doi.org\/10.1145\/2499370.2462190","DOI":"10.1145\/2499370.2462190"},{"key":"27_CR5","doi-asserted-by":"publisher","unstructured":"Apinis, K., Vene, V., Vojdani, V.: Demand-driven interprocedural analysis for map-based abstract domains. Journal of Logical and Algebraic Methods in Programming 100, 57\u201370 (2018), https:\/\/doi.org\/10.1016\/j.jlamp.2018.06.003","DOI":"10.1016\/j.jlamp.2018.06.003"},{"key":"27_CR6","doi-asserted-by":"publisher","unstructured":"Apinis, K., Vojdani, V.: Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis. Zenodo. (2023), https:\/\/doi.org\/10.5281\/zenodo.7560511, (Software artifact)","DOI":"10.5281\/zenodo.7560511"},{"key":"27_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: Exchanging verification results between verifiers. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 326\u2013337, FSE 2016, ACM (2016), https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"27_CR8","doi-asserted-by":"publisher","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, ESEC\/FSE, ACM (Aug 2015), https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Birkhoff, G.: Lattice theory, vol.\u00a025. American Mathematical Soc. (1940)","DOI":"10.1090\/coll\/025"},{"key":"27_CR10","doi-asserted-by":"publisher","unstructured":"Campion, M., Dalla\u00a0Preda, M., Giacobazzi, R.: Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis. Proceedings of the ACM on Programming Languages 6(POPL), 59:1\u201359:31 (Jan 2022), https:\/\/doi.org\/10.1145\/3498721","DOI":"10.1145\/3498721"},{"key":"27_CR11","doi-asserted-by":"publisher","unstructured":"Chang, B.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: VMCAI\u201905, LNCS, vol. 3385, pp. 147\u2013163, Springer (2005), https:\/\/doi.org\/10.1007\/978-3-540-30579-8_11","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"27_CR12","doi-asserted-by":"publisher","unstructured":"Christakis, M., Bird, C.: What Developers Want and Need from Program Analysis: An Empirical Study. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, pp. 332\u2013343, ASE 2016, ACM (2016), https:\/\/doi.org\/10.1145\/2970276.2970347","DOI":"10.1145\/2970276.2970347"},{"key":"27_CR13","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: Algorithmic verification and debugging. Commun. ACM 52(11), 74\u201384 (nov 2009), https:\/\/doi.org\/10.1145\/1592761.1592781","DOI":"10.1145\/1592761.1592781"},{"key":"27_CR14","doi-asserted-by":"publisher","unstructured":"Consel, C., Khoo, S.C.: Parameterized partial evaluation. ACM Transactions on Programming Languages and Systems 15(3), 463\u2013493 (Jul 1993), https:\/\/doi.org\/10.1145\/169683.174155","DOI":"10.1145\/169683.174155"},{"key":"27_CR15","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: 4th ACM Symp. on Principles of Programming Languages (POPL\u201977), pp. 238\u2013252, ACM Press (1977), https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"27_CR16","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interpretation. ACM SIGPLAN Notices 37(1), 178\u2013190 (Jan 2002), https:\/\/doi.org\/10.1145\/565816.503290","DOI":"10.1145\/565816.503290"},{"key":"27_CR17","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Combination of abstractions in the astr\u00e9e static analyzer. In: ASIAN\u201906, LNCS, vol. 4435, pp. 272\u2013300, Springer (2006), https:\/\/doi.org\/10.1007\/978-3-540-77505-8_23","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"27_CR18","doi-asserted-by":"publisher","unstructured":"Cousot, P., Giacobazzi, R., Ranzato, F.: A2I: Abstract2 Interpretation. Proceedings of the ACM on Programming Languages 3(POPL), 42:1\u201342:31 (Jan 2019), https:\/\/doi.org\/10.1145\/3290355","DOI":"10.1145\/3290355"},{"key":"27_CR19","doi-asserted-by":"publisher","unstructured":"Dom\u00e9nech, J.J., Gallagher, J.P., Genaim, S.: Control-flow refinement by partial evaluation, and its application to termination and cost analysis. Theory and Practice of Logic Programming 19(5-6), 990\u20131005 (2019), https:\/\/doi.org\/10.1017\/S1471068419000310","DOI":"10.1017\/S1471068419000310"},{"key":"27_CR20","doi-asserted-by":"publisher","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: An abstract domain of uninterpreted functions. In: VMCAI\u201905, LNCS, vol. 9583, pp. 85\u2013103, Springer (2016), https:\/\/doi.org\/10.1007\/978-3-662-49122-5_4","DOI":"10.1007\/978-3-662-49122-5_4"},{"key":"27_CR21","doi-asserted-by":"publisher","unstructured":"Giacobazzi, R., Logozzo, F., Ranzato, F.: Analyzing program analyses. In: POPL \u201915, pp. 261\u2013273, ACM Press (Jan 2015), https:\/\/doi.org\/10.1145\/2676726.2676987","DOI":"10.1145\/2676726.2676987"},{"key":"27_CR22","doi-asserted-by":"publisher","unstructured":"Johnson, B., Song, Y., Murphy-Hill, E., Bowdidge, R.: Why Don\u2019t Software Developers Use Static Analysis Tools to Find Bugs? In: Proceedings of the 2013 International Conference on Software Engineering, pp. 672\u2013681, ICSE \u201913, IEEE Press (2013), https:\/\/doi.org\/10.1109\/ICSE.2013.6606613","DOI":"10.1109\/ICSE.2013.6606613"},{"key":"27_CR23","doi-asserted-by":"publisher","unstructured":"Jones, N.D.: Combining abstract interpretation and partial evaluation (brief overview). In: Van\u00a0Hentenryck, P. (ed.) Static Analysis, pp. 396\u2013405, LNCS, Springer, Berlin, Heidelberg (1997), https:\/\/doi.org\/10.1007\/BFb0032761","DOI":"10.1007\/BFb0032761"},{"key":"27_CR24","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial evaluation and automatic program generation. Prentice-Hall (1993)"},{"key":"27_CR25","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: VMCAI\u201906, LNCS, vol. 3855, pp. 348\u2013363, Springer (2006), https:\/\/doi.org\/10.1007\/11609773_23","DOI":"10.1007\/11609773_23"},{"key":"27_CR26","doi-asserted-by":"publisher","unstructured":"Nachtigall, M., Nguyen Quang\u00a0Do, L., Bodden, E.: Explaining static analysis \u2014 A perspective. In: ASEW\u201919, pp. 29\u201332 (Nov 2019), https:\/\/doi.org\/10.1109\/ASEW.2019.00023","DOI":"10.1109\/ASEW.2019.00023"},{"key":"27_CR27","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 106\u2013119, POPL \u201997, ACM (1997), https:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"27_CR28","doi-asserted-by":"publisher","unstructured":"Nguyen Quang\u00a0Do, L., Bodden, E.: Explaining static analysis with rule graphs. IEEE Transactions on Software Engineering (Jan 2020), https:\/\/doi.org\/10.1109\/TSE.2020.2999534","DOI":"10.1109\/TSE.2020.2999534"},{"key":"27_CR29","doi-asserted-by":"publisher","unstructured":"Puebla, G., Albert, E., Hermenegildo, M.: Abstract Interpretation with Specialized Definitions. In: Yi, K. (ed.) Static Analysis, pp. 107\u2013126, LNCS, Springer, Berlin, Heidelberg (2006), ISBN 978-3-540-37758-0, https:\/\/doi.org\/10.1007\/11823230_8","DOI":"10.1007\/11823230_8"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Seidl, H., Vene, V., M\u00fcller-Olm, M.: Global invariants for analyzing multithreaded applications. Proc. of the Estonian Academy of Sciences: Phys., Math. 52(4), 413\u2013436 (2003), ISSN 1406-0086","DOI":"10.3176\/phys.math.2003.4.05"},{"key":"27_CR31","doi-asserted-by":"publisher","unstructured":"Seidl, H., Vogler, R.: Three improvements to the top-down solver. In: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP \u201918, ACM (2018), https:\/\/doi.org\/10.1145\/3236950.3236967","DOI":"10.1145\/3236950.3236967"},{"key":"27_CR32","doi-asserted-by":"publisher","unstructured":"Seidl, H., Wilhelm, R., Hack, S.: Compiler Design: Analysis and Transformation. Springer Science & Business Media (2012), https:\/\/doi.org\/10.1007\/978-3-642-17548-0","DOI":"10.1007\/978-3-642-17548-0"},{"key":"27_CR33","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Application, pp. 189\u2013233, Prentice-Hall (1981)"},{"key":"27_CR34","doi-asserted-by":"publisher","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the goblint approach. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016, pp. 391\u2013402, ACM (2016), https:\/\/doi.org\/10.1145\/2970276.2970337","DOI":"10.1145\/2970276.2970337"},{"key":"27_CR35","doi-asserted-by":"publisher","unstructured":"Zhang, X., Grigore, R., Si, X., Naik, M.: Effective interactive resolution of static analysis alarms. Proceedings of the ACM on Programming Languages 1(OOPSLA), 1\u201330 (Oct 2017), https:\/\/doi.org\/10.1145\/3133881","DOI":"10.1145\/3133881"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30820-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:06:32Z","timestamp":1690974392000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"169","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":"56","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":"6","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":"33% - 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":"11","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)"}}]}}