{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:05:35Z","timestamp":1784797535351,"version":"3.55.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325365","type":"print"},{"value":"9783032325372","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Consistency-based diagnosis is a formal approach to software fault localization that explains failing executions by identifying program components whose modification would restore correctness. Tools such as\n                    <jats:sc>BugAssist<\/jats:sc>\n                    and (more recently)\n                    <jats:sc>CFaults<\/jats:sc>\n                    instantiate this idea using logical encodings and bounded model checking.\n                  <\/jats:p>\n                  <jats:p>\n                    In our first contribution, we improve on this line of work. We present\n                    <jats:sc>SherLoc<\/jats:sc>\n                    , a consistency-based diagnosis engine for ANSI-C programs with multiple failing test cases.\n                    <jats:sc>SherLoc<\/jats:sc>\n                    introduces an explicit repair model that supports pointers and arrays, ensuring that diagnoses correspond only to semantically valid C repairs. In addition, we adapt efficient algorithms from hardware diagnosis, which avoid costly self-composition, and significantly outperform existing tools on standard benchmarks.\n                  <\/jats:p>\n                  <jats:p>In our second contribution, we expose fundamental limitations of formal fault localization: program optimizations and transformations can invalidate diagnoses despite semantic equivalence, representing a major hurdle to further scalability improvements; function inlining can break the functional consistency of repairs, yielding diagnoses that cannot be realized at the source level; and bounded encodings inherently miss diagnoses in the presence of loops or unbounded behavior. Our exposition clarifies the gap between the formal ideal of sound and complete diagnosis and what current techniques can realistically guarantee, and thereby helps guide future work toward more robust and principled approaches.<\/jats:p>","DOI":"10.1007\/978-3-032-32537-2_10","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:43:27Z","timestamp":1784796207000},"page":"207-229","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Consistency-Based Software Diagnosis: Accuracy, Scalability, and\u00a0Limitations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6828-659X","authenticated-orcid":false,"given":"Sarah","family":"Sallinger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lukas","family":"Graussam","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0143-632X","authenticated-orcid":false,"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4535-2902","authenticated-orcid":false,"given":"Alexey","family":"Ignatiev","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/S10270-017-0612-Y","volume":"18","author":"G Birch","year":"2019","unstructured":"Birch, G., Fischer, B., Poppleton, M.: Fast test suite-driven model-based fault localisation with application to pinpointing defects in student programs. Softw. Syst. Model. 18(1), 445\u2013471 (2019). https:\/\/doi.org\/10.1007\/S10270-017-0612-Y","journal-title":"Softw. Syst. Model."},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02988, pp. 168\u2013176. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Console, L., Friedrich, G., Dupr\u00e9, D.T.: Model-based diagnosis meets error diagnosis in logic programs. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 1494\u20131501 Morgan Kaufmann (1993)","DOI":"10.1007\/BFb0019402"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Cytron, R., Lowry, A., Zadeck, F.K.: Code motion of control structures in high-level languages. In: Principles of Programming Languages (POPL), pp. 70\u201385. ACM Press (1986). https:\/\/doi.org\/10.1145\/512644.512651","DOI":"10.1145\/512644.512651"},{"issue":"8","key":"10_CR5","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). https:\/\/doi.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"issue":"4","key":"10_CR6","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/S10664-005-3861-2","volume":"10","author":"H Do","year":"2005","unstructured":"Do, H., Elbaum, S.G., Rothermel, G.: Supporting controlled experimentation with testing techniques: an infrastructure and its potential impact. Empir. Softw. Eng. 10(4), 405\u2013435 (2005). https:\/\/doi.org\/10.1007\/S10664-005-3861-2","journal-title":"Empir. Softw. Eng."},{"issue":"6","key":"10_CR7","doi-asserted-by":"publisher","first-page":"1138","DOI":"10.1109\/TCAD.2008.923234","volume":"27","author":"G Fey","year":"2008","unstructured":"Fey, G., Staber, S., Bloem, R., Drechsler, R.: Automatic fault localization for property checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(6), 1138\u20131149 (2008). https:\/\/doi.org\/10.1109\/TCAD.2008.923234","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Graussam, L.: Consistency-based software fault localization with multiple observations. Diploma thesis, Technische Universit\u00e4t Wien (2024). https:\/\/doi.org\/10.34726\/hss.2024.109000, https:\/\/doi.org\/10.34726\/hss.2024.109000","DOI":"10.34726\/hss.2024.109000"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Griesmayer, A., Staber, S., Bloem, R.: Automated Fault Localization for C Programs. In: Bloem, R., Roveri, M., Somenzi, F. (eds.) Verification and Debugging (V&D@FLoC). ENTCS, vol.\u00a0174, pp. 95\u2013111. Elsevier (2006). https:\/\/doi.org\/10.1016\/J.ENTCS.2006.12.032","DOI":"10.1016\/J.ENTCS.2006.12.032"},{"issue":"2","key":"10_CR10","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1002\/STVR.421","volume":"20","author":"A Griesmayer","year":"2010","unstructured":"Griesmayer, A., Staber, S., Bloem, R.: Fault localization using a model checker. Softw. Test. Verification Reliab. 20(2), 149\u2013173 (2010). https:\/\/doi.org\/10.1002\/STVR.421","journal-title":"Softw. Test. Verification Reliab."},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Groce, A.: Error Explanation with Distance Metrics. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02988, pp. 108\u2013122. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_8","DOI":"10.1007\/978-3-540-24730-2_8"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Hutchins, M., Foster, H., Goradia, T., Ostrand, T.: Experiments on the effectiveness of dataflow- and control-flow-based test adequacy criteria. In: International Conference on Software Engineering (ICSE), pp. 191\u2013200 (1994). https:\/\/doi.org\/10.1109\/ICSE.1994.296778","DOI":"10.1109\/ICSE.1994.296778"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Ignatiev, A., Morgado, A., Weissenbacher, G., Marques-Silva, J.: Model-based diagnosis with multiple observations. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 1108\u20131115. ijcai.org (2019). https:\/\/doi.org\/10.24963\/IJCAI.2019\/155","DOI":"10.24963\/IJCAI.2019\/155"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441\u2013460 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.05.005, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0022000011000547, games in Verification","DOI":"10.1016\/j.jcss.2011.05.005"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Jose, M., Majumdar, R.: Bug-assist: assisting fault localization in ANSI-C programs. In: Computer Aided Verification (CAV). LNCS, vol.\u00a06806, pp. 504\u2013509. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_40","DOI":"10.1007\/978-3-642-22110-1_40"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Programming Language Design and Implementation (PLDI), pp. 437\u2013446. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993550","DOI":"10.1145\/1993498.1993550"},{"key":"10_CR17","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer (2008)"},{"issue":"1","key":"10_CR18","doi-asserted-by":"publisher","first-page":"88","DOI":"10.2197\/IPSJJIP.24.88","volume":"24","author":"S Lamraoui","year":"2016","unstructured":"Lamraoui, S., Nakajima, S.: A formula-based approach for automatic fault localization of multi-fault programs. J. Inf. Process. 24(1), 88\u201398 (2016). https:\/\/doi.org\/10.2197\/IPSJJIP.24.88","journal-title":"J. Inf. Process."},{"key":"10_CR19","unstructured":"Lewis, D.: Counterfactuals. Wiley-Blackwell (2001)"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Li, Y., Wang, S., Nguyen, T.N.: Fault localization to detect co-change fixing locations, pp. 659\u2013671. Foundations of Software Engineering (FSE), ACM (2022). https:\/\/doi.org\/10.1145\/3540250.3549137","DOI":"10.1145\/3540250.3549137"},{"key":"10_CR21","unstructured":"Menc\u00eda, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 1973\u20131979. AAAI Press (2015). http:\/\/ijcai.org\/Abstract\/15\/280"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Orvalho, P., Janota, M., Manquinho, V.M.: Cfaults: model-based diagnosis for fault localization in C with multiple test cases. In: Symposium on Formal Methods (FM). LNCS, vol. 14933, pp. 463\u2013481 Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_24","DOI":"10.1007\/978-3-031-71162-6_24"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Orvalho, P., Janota, M., Manquinho, V.: C-Pack of IPAs: A C90 program benchmark of introductory programming assignments, pp. 14\u201321. APR \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3643788.3648010","DOI":"10.1145\/3643788.3648010"},{"issue":"1","key":"10_CR24","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57\u201395 (1987). https:\/\/doi.org\/10.1016\/0004-3702(87)90062-2","journal-title":"Artif. Intell."},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Rothenberg, B.C., Grumberg, O.: Must fault localization for program repair. In: Computer Aided Verification (CAV), pp. 658\u2013680. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_33","DOI":"10.1007\/978-3-030-53291-8_33"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Safarpour, S., Mangassarian, H., Veneris, A., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: Formal Methods in Computer Aided Design (FMCAD\u201907), pp. 13\u201319 (2007). https:\/\/doi.org\/10.1109\/FAMCAD.2007.26","DOI":"10.1109\/FAMCAD.2007.26"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Sallinger, S., Graussam, L., Weissenbacher, G., Zuleger, F., Ignatiev, A.: SherLoc artifact: Consistency-based software diagnosis: accuracy, scalability, and limitations (2026). https:\/\/doi.org\/10.5281\/zenodo.19798981","DOI":"10.5281\/zenodo.19798981"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Sallinger, S., Weissenbacher, G., Zuleger, F.: A formalization of heisenbugs and their causes. In: Software Engineering and Formal Methods (SEFM). LNCS, vol. 14323, pp. 282\u2013300. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47115-5_16","DOI":"10.1007\/978-3-031-47115-5_16"},{"key":"10_CR29","unstructured":"Sallinger, S.S.: Rigorous Debugging Techniques for Software Systems. Ph.D. thesis, TU Wien (2026)"},{"issue":"10","key":"10_CR30","doi-asserted-by":"publisher","first-page":"1606","DOI":"10.1109\/TCAD.2005.852031","volume":"24","author":"A Smith","year":"2005","unstructured":"Smith, A., Veneris, A., Ali, M., Viglas, A.: Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(10), 1606\u20131621 (2005). https:\/\/doi.org\/10.1109\/TCAD.2005.852031","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"Welsh, M.: The end of programming. Commun. ACM 66(1), 34\u201335 (Dec 2022). https:\/\/doi.org\/10.1145\/3570220","DOI":"10.1145\/3570220"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F., Li, D.: Software fault localization: an overview of research, techniques, and tools, chap.\u00a01, pp. 1\u2013117. John Wiley & Sons, Ltd (2023). https:\/\/doi.org\/10.1002\/9781119880929.ch1","DOI":"10.1002\/9781119880929.ch1"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Wotawa, F., Stumptner, M., Mayer, W.: Model-based debugging or how to diagnose programs automatically. In: Developments in Applied Artificial Intelligence, International Conference on Industrial and Engineering, Applications of Artificial Intelligence and Expert Systems (IEA\/AIE). LNCS, vol.\u00a02358, pp. 746\u2013757. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-48035-8_72","DOI":"10.1007\/3-540-48035-8_72"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Yang, A.Z.H., Le Goues, C., Martins, R., Hellendoorn, V.J.: Large language models for test-free fault localization. In: International Conference on Software Engineering (ICSE), pp. 17:1\u201317:12. ACM (2024). https:\/\/doi.org\/10.1145\/3597503.3623342","DOI":"10.1145\/3597503.3623342"},{"issue":"1","key":"10_CR35","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1049\/IET-SEN.2018.5137","volume":"13","author":"A Zakari","year":"2019","unstructured":"Zakari, A., Lee, S.P., Alam, K.A., Ahmad, R.: Software fault localisation: a systematic mapping study. IET Softw. 13(1), 60\u201374 (2019). https:\/\/doi.org\/10.1049\/IET-SEN.2018.5137","journal-title":"IET Softw."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32537-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:43:37Z","timestamp":1784796217000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32537-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325365","9783032325372"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32537-2_10","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":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}