{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T16:35:44Z","timestamp":1772642144949,"version":"3.50.1"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,11,9]],"date-time":"2022-11-09T00:00:00Z","timestamp":1667952000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,11,9]],"date-time":"2022-11-09T00:00:00Z","timestamp":1667952000000},"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":["Computing"],"published-print":{"date-parts":[[2023,2]]},"DOI":"10.1007\/s00607-022-01130-0","type":"journal-article","created":{"date-parts":[[2022,11,9]],"date-time":"2022-11-09T22:02:38Z","timestamp":1668031358000},"page":"321-351","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Constraint-based debugging in probabilistic model checking"],"prefix":"10.1007","volume":"105","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0339-1903","authenticated-orcid":false,"given":"Hichem","family":"Debbi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,11,9]]},"reference":[{"issue":"1","key":"1130_CR1","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/s10703-011-0132-2","volume":"40","author":"I Beer","year":"2012","unstructured":"Beer I, Ben-David S, Chockler H, Orni A, Treer R (2012) Explaining counterexamples using causality. Formal Methods Syst Design 40(1):20\u201340","journal-title":"Formal Methods Syst Design"},{"key":"1130_CR2","doi-asserted-by":"crossref","unstructured":"Zeller A (1999) Yesterday, my program worked. today, it does not. why? In: ACM symposium on the foundations of software engineering, pp 253\u2013267","DOI":"10.1007\/3-540-48166-4_16"},{"key":"1130_CR3","doi-asserted-by":"crossref","unstructured":"Wang C, Yang Z, Ivancic F, Gupta A (2006) Whodunit? causal analysis for counterexamples. In: 4th international symposium, ATVA. LNCS, vol 4218, Springer, Berlin, Heidelberg, pp 82\u201395","DOI":"10.1007\/11901914_9"},{"key":"1130_CR4","doi-asserted-by":"crossref","unstructured":"Groce A (2005) Error Explanation and Fault Localization with Distance Metrics. PhD thesis, School of Computer Science, Carnegie Mellon University","DOI":"10.1007\/978-3-540-24730-2_8"},{"issue":"5","key":"1130_CR5","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) Logic for reasoning about time and reliability. Formal Asp Comput 6(5):512\u2013535","journal-title":"Formal Asp Comput"},{"issue":"1","key":"1130_CR6","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model-checking continuous-time Markov chains. ACM Trans Comput Log 1(1):162\u2013170","journal-title":"ACM Trans Comput Log"},{"issue":"7","key":"1130_CR7","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier C, Haverkort B, Hermanns H, Katoen JP (2003) Model checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29(7):524\u2013541","journal-title":"IEEE Trans Softw Eng"},{"key":"1130_CR8","unstructured":"Debbi H, Bourahla M (2013) Causal analysis of probabilistic counterexamples. In: Proceedings of the eleventh ACM-IEEE international conference on formal methods and models for codesign (Memocode), pp 77\u201386"},{"key":"1130_CR9","doi-asserted-by":"crossref","unstructured":"Debbi H (2016) Debugging of markov decision processes (mdps) models. In: Proceedings of the first workshop on causal reasoning for embedded and safety-critical systems, pp 25\u201339","DOI":"10.4204\/EPTCS.224.4"},{"key":"1130_CR10","doi-asserted-by":"crossref","unstructured":"Wimmer R, Jansen N, Vorpahl A (2013) High-level counterexamples for probabilistic automata. In: Quantitative evaluation of systems (QEST). LNCS, vol 8054, Springer, Berlin, Heidelberg, pp 39\u201354","DOI":"10.1007\/978-3-642-40196-1_4"},{"key":"1130_CR11","doi-asserted-by":"crossref","unstructured":"Kleer J, Kurien J (2003) Fundamentals of model-based diagnosis. In: IFAC Proceedings Volumes, vol 36, Sciencedirect pp 25\u201336","DOI":"10.1016\/S1474-6670(17)36467-4"},{"issue":"8","key":"1130_CR12","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1109\/TSE.2016.2521368","volume":"42","author":"WE Wong","year":"2016","unstructured":"Wong WE, Gao R, Li Y, Abreu R, Wotawa F (2016) A survey on software fault localization. IEEE Trans Softw Eng 42(8):707\u2013740","journal-title":"IEEE Trans Softw Eng"},{"key":"1130_CR13","unstructured":"Nica M (2010) On the Use of Constraints in Automated Program Debugging - From Foundations to Empirical Results. PhD thesis, Graz University of Technology"},{"issue":"1","key":"1130_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0004-3702(99)00034-X","volume":"111","author":"G Friedrich","year":"1999","unstructured":"Friedrich G, Stumptner M, Wotawa F (1999) Model-based diagnosis of hardware designs. Artif Intell 111(1):3\u201339","journal-title":"Artif Intell"},{"key":"1130_CR15","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J Ferrante","year":"1987","unstructured":"Ferrante J, Ottenstein K, Warren J (1987) The program dependence graph and its use in optimization. ACM Trans Program Lang Syst (TOPLAS) 9:319\u2013349","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"key":"1130_CR16","unstructured":"Weiser M (1981) Program slicing. In: Proceeding ICSE \u201981 Proceedings of the 5th international conference on Software engineering, IEEE Press Piscataway, pp 439\u2013449"},{"key":"1130_CR17","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/s100090050041","volume":"2","author":"L Millett","year":"2000","unstructured":"Millett L, Teitelbaum T (2000) Issues in slicing promela and its applications to model checking, protocol understanding, and simulation. Int J Softw Tools Technol Transfer 2:443\u2013449","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"1130_CR18","doi-asserted-by":"crossref","unstructured":"Hinton A, Kwiatkowska M, Norman G, Parker D (2006) Prism: a tool for automatic verification of probabilistic systems. In: Proceedings of TACAS, Springer, Berlin, Heidelberg, pp 441\u2013444","DOI":"10.1007\/11691372_29"},{"key":"1130_CR19","doi-asserted-by":"crossref","unstructured":"Aljazzar H, Leitner-Fischer F, Leue S, Simeonov D (2011) Dipro - a tool for probabilistic counterexample generation. In: Proceedings of the 18th international SPIN Workshop. LNCS 6823, Springer, Berlin, Heidelberg, pp 183\u2013187","DOI":"10.1007\/978-3-642-22306-8_13"},{"issue":"1","key":"1130_CR20","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/TSE.2009.57","volume":"36","author":"H Aljazzar","year":"2010","unstructured":"Aljazzar H, Leue S (2010) Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans Softw Eng 36(1):37\u201360","journal-title":"IEEE Trans Softw Eng"},{"issue":"2","key":"1130_CR21","first-page":"72","volume":"35","author":"T Han","year":"2009","unstructured":"Han T, Katoen J (2009) Counterexamples generation in probabilistic model checking. IEEE Trans Softw Eng 35(2):72\u201386","journal-title":"IEEE Trans Softw Eng"},{"key":"1130_CR22","doi-asserted-by":"crossref","unstructured":"Clarke EM (2008) In: The birth of model checking. Springer-Verlag, pp 1\u201326","DOI":"10.1007\/978-3-540-69850-0_1"},{"key":"1130_CR23","unstructured":"Mayer W, Stumptner M, Wieland D, Wotawa F (2000) Can AI help to improve debugging substantially? debugging experiences with value-based models. In: Proceedings of the European conference on artificial intelligence (ECAI), IOS Press, pp 417\u2013421"},{"issue":"4","key":"1130_CR24","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1016\/j.jlap.2012.03.002","volume":"81","author":"F Wotawa","year":"2012","unstructured":"Wotawa F, Nica M, Moraru I (2012) Automated debugging based on a constraint model of the program and a test case. J Logic Algebr Program 81(4):390\u2013407","journal-title":"J Logic Algebr Program"},{"issue":"2","key":"1130_CR25","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s11219-014-9236-4","volume":"23","author":"R Abreu","year":"2015","unstructured":"Abreu R, Hofer B, Perez A, Wotawa F (2015) Using constraints to diagnose faulty spreadsheets. Softw Qual J 23(2):297\u2013322","journal-title":"Softw Qual J"},{"key":"1130_CR26","unstructured":"Wotawa F (2008) Bridging the gap between slicing and model-based diagnosis. In: Proceedings of the 20th international conference on software engineering and knowledge engineering (SEKE), pp 836\u2013841"},{"key":"1130_CR27","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1016\/S0004-3702(01)00161-8","volume":"135","author":"F Wotawa","year":"2002","unstructured":"Wotawa F (2002) On the relationship between model-based debugging and program slicing. Artif Intell 135:124\u2013143","journal-title":"Artif Intell"},{"key":"1130_CR28","unstructured":"Grammatech: https:\/\/resources.grammatech.com\/"},{"key":"1130_CR29","unstructured":"Wisconsin: http:\/\/www.cs.wisc.edu\/wpis\/slicing_tool\/"},{"key":"1130_CR30","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1109\/TSE.2009.87","volume":"36","author":"G Baah","year":"2010","unstructured":"Baah G, Podgurski A, Harrold MJ (2010) The probabilistic program dependence graph and its application to fault diagnosis. IEEE Trans Software Eng 36:528\u2013545","journal-title":"IEEE Trans Software Eng"},{"key":"1130_CR31","doi-asserted-by":"crossref","unstructured":"Gulwani S, Srivastava S, Venkatesan R (2008) Program analysis as constraint solving. In: SIGPLAN Not, vol 43(6). pp 281\u2013292","DOI":"10.1145\/1379022.1375616"},{"key":"1130_CR32","unstructured":"Keng B, Veneris A (2012) Automated debugging of missing input constraints in a formal verification environment. In: Proceedings of the 12th conference on formal methods in computer-aided design (FMCAD 2012), IEEE, pp 101\u2013105"},{"key":"1130_CR33","doi-asserted-by":"crossref","unstructured":"Collavizza H, Vinh NL, Rueher M, Devulder S, Gueguen T (2011) A dynamic constraint-based bmc strategy for generating counterexamples. In: Proceedings of the 2011 ACM symposium on applied computing. SAC \u201911, pp 1633\u20131638","DOI":"10.1145\/1982185.1982528"},{"key":"1130_CR34","doi-asserted-by":"crossref","unstructured":"Bekkouche M, Collavizza H, Rueher M (2015) Locfaults: a new flow-driven and constraint-based error localization approach. In: Proceedings of the 30th annual ACM symposium on applied computing. SAC \u201915, New York, NY, USA, pp 1773\u20131780","DOI":"10.1145\/2695664.2695822"},{"key":"1130_CR35","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-96145-3_15","volume-title":"Computer aided verification","author":"A Abate","year":"2018","unstructured":"Abate A, David C, Kesseli P, Kroening D, Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: Chockler H, Weissenbacher G (eds) Computer aided verification. Springer, Cham, pp 270\u2013288"},{"key":"1130_CR36","doi-asserted-by":"crossref","unstructured":"Aljazzar H, Leue S (2009) Generation of counterexamples for model checking of markov decision processes. In: Proceedings of the international conference on quantitative evaluation of systems (QEST), pp 197\u2013206","DOI":"10.1109\/QEST.2009.10"},{"key":"1130_CR37","unstructured":"Halpern J, Pearl J (2001) Causes and explanations: a structural-model approach part i: Causes. In: Proceedings of the 17th UAI, pp 194\u2013202"},{"issue":"1","key":"1130_CR38","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1613\/jair.1391","volume":"22","author":"H Chockler","year":"2004","unstructured":"Chockler H, Halpern JY (2004) Responsibility and blame: a structural model approach. J Artif Intell Res (JAIR) 22(1):93\u2013115","journal-title":"J Artif Intell Res (JAIR)"},{"key":"1130_CR39","doi-asserted-by":"crossref","unstructured":"Wimmer R, Jansen N, Abraham E, Becker B, Katoen J (2012) Minimal critical subsystems for discrete-time markov models. In: TACAS. LNCS, vol 7214, Springer, Berlin, Heidelberg, pp 299\u2013314","DOI":"10.1007\/978-3-642-28756-5_21"},{"issue":"2","key":"1130_CR40","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1504\/IJCCBS.2013.056492","volume":"4","author":"F Leitner-Fischer","year":"2013","unstructured":"Leitner-Fischer F, Leue S (2013) Probabilistic fault tree synthesis using causality computation. Int J Crit Comput Based Syst 4(2):119\u2013143","journal-title":"Int J Crit Comput Based Syst"},{"key":"1130_CR41","unstructured":"PRISM: https:\/\/www.prismmodelchecker.org\/manual\/ThePRISMLanguage\/Introduction"},{"issue":"18","key":"1130_CR42","doi-asserted-by":"publisher","first-page":"2129","DOI":"10.1016\/j.artint.2011.07.003","volume":"175","author":"H Aljazzar","year":"2011","unstructured":"Aljazzar H, Leue S (2011) K*: a heuristic search algorithm for finding the k shortest paths. Artif Intell 175(18):2129\u20132154","journal-title":"Artif Intell"},{"key":"1130_CR43","doi-asserted-by":"crossref","unstructured":"Katoen JP, Khattri M, Zapreev IS (2005) A markov reward model checker. In: Proceedings of QEST. pp 243\u2013244","DOI":"10.1109\/QEST.2005.2"},{"key":"1130_CR44","unstructured":"Polling: http:\/\/www.prismmodelchecker.org\/casestudies\/polling.php"},{"key":"1130_CR45","doi-asserted-by":"publisher","first-page":"1649","DOI":"10.1109\/49.62852","volume":"8","author":"O Ibe","year":"1990","unstructured":"Ibe O, Trivedi K (1990) Stochastic Petri net models of polling systems. IEEE J Sel Areas Commun 8:1649\u20131657","journal-title":"IEEE J Sel Areas Commun"},{"key":"1130_CR46","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"L de Moura","year":"2008","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin Heidelberg, pp 337\u2013340"},{"key":"1130_CR47","unstructured":"NAND: http:\/\/www.prismmodelchecker.org\/\/casestudies\/nand.php"},{"key":"1130_CR48","unstructured":"CSMA: https:\/\/www.prismmodelchecker.org\/casestudies\/csma.php"},{"key":"1130_CR49","unstructured":"PRISM: http:\/\/www.prismmodelchecker.org\/benchmarks\/models.php"},{"key":"1130_CR50","unstructured":"EGL: https:\/\/www.prismmodelchecker.org\/tutorial\/egl.php"},{"key":"1130_CR51","unstructured":"Crowds: https:\/\/www.prismmodelchecker.org\/casestudies\/crowds.php"},{"key":"1130_CR52","unstructured":"Zeroconf: https:\/\/www.prismmodelchecker.org\/casestudies\/zeroconf.php"},{"key":"1130_CR53","doi-asserted-by":"crossref","unstructured":"Fischer F, Leue S (2013) Causality checking for complex system models. In: Proceedings of verification, model checking, and abstract interpretation (VMCAI). LNCS 7737, Springer, Berlin, Heidelberg, pp 248\u2013276","DOI":"10.1007\/978-3-642-35873-9_16"},{"key":"1130_CR54","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/j.jss.2018.05.013","volume":"143","author":"R Calinescu","year":"2018","unstructured":"Calinescu R, \u010ce\u0161ka M, Gerasimou S, Kwiatkowska M, Paoletti N (2018) Efficient synthesis of robust models for stochastic systems. J Syst Softw 143:140\u2013158","journal-title":"J Syst Softw"},{"key":"1130_CR55","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.ic.2018.02.019","volume":"259","author":"G Chatzieleftheriou","year":"2018","unstructured":"Chatzieleftheriou G, Katsaros P (2018) Abstract model repair for probabilistic systems. Inf Comput 259:142\u2013160","journal-title":"Inf Comput"},{"key":"1130_CR56","doi-asserted-by":"crossref","unstructured":"Li X, Li W, Zhang Y, Zhang L (2019) Deepfl: integrating multiple fault diagnosis dimensions for deep fault localization. In: Proceedings of the 28th ACM SIGSOFT international symposium on software testing and analysis, pp 169\u2013180","DOI":"10.1145\/3293882.3330574"},{"key":"1130_CR57","doi-asserted-by":"crossref","unstructured":"Lou Y, Ghanbari A, Li X, Zhang L, Zhang H, Hao D, Zhang L (2020) Can automated program repair refine fault localization? a unified debugging approach. In: Proceedings of the 29th ACM SIGSOFT international symposium on software testing and analysis. ISSTA 2020, pp 75\u201387","DOI":"10.1145\/3395363.3397351"}],"container-title":["Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-022-01130-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00607-022-01130-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-022-01130-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T16:16:20Z","timestamp":1675181780000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00607-022-01130-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,9]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,2]]}},"alternative-id":["1130"],"URL":"https:\/\/doi.org\/10.1007\/s00607-022-01130-0","relation":{},"ISSN":["0010-485X","1436-5057"],"issn-type":[{"value":"0010-485X","type":"print"},{"value":"1436-5057","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,9]]},"assertion":[{"value":"27 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 October 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 November 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}