{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:10:07Z","timestamp":1759018207962,"version":"3.44.0"},"reference-count":32,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Systems and Software"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1016\/j.jss.2023.111897","type":"journal-article","created":{"date-parts":[[2023,11,14]],"date-time":"2023-11-14T15:27:02Z","timestamp":1699975622000},"page":"111897","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Localizing faults using verification technique"],"prefix":"10.1016","volume":"209","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9327-9677","authenticated-orcid":false,"given":"Sudakshina","family":"Dutta","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jss.2023.111897_b1","series-title":"HandBook of Automated Reasoning, vol. 2","first-page":"445","article-title":"Unification theory","author":"Baader","year":"2001"},{"issue":"4","key":"10.1016\/j.jss.2023.111897_b2","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1109\/TSE.2009.87","article-title":"The probabilistic program dependence graph and its application to fault diagnosis","volume":"36","author":"Baah","year":"2010","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.jss.2023.111897_b3","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S., 2003. From symptom to cause: Localizing errors in counterexample traces. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New Orleans, Louisisana, USA, pp. 97\u2014105.","DOI":"10.1145\/604131.604140"},{"issue":"5","key":"10.1016\/j.jss.2023.111897_b4","doi-asserted-by":"crossref","first-page":"847","DOI":"10.1016\/j.jlamp.2016.05.004","article-title":"Product programs and relational program logics","volume":"85","author":"Barthe","year":"2016","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"6","key":"10.1016\/j.jss.2023.111897_b5","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/1041685.1029908","article-title":"Explaining abstract counterexamples","volume":"29","author":"Chaki","year":"2004","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"10.1016\/j.jss.2023.111897_b6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Lerda, F., 2004. A Tool for Checking ANSI-C Programs. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, TACAS. pp. 168\u2014176.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"10.1016\/j.jss.2023.111897_b7","unstructured":"Cristinel, M., Stumptner, M., Wotawa, F., 2000. Modeling Java Programs for Diagnosis. In: Proceedings of the 14th European Conference on Artificial Intelligence, ECAI. Berlin, Germany, pp. 171\u2013175."},{"key":"10.1016\/j.jss.2023.111897_b8","doi-asserted-by":"crossref","unstructured":"Darke, P., Chimdyalwar, B., Venkatesh, R., Shrotri, U., Metta, R., 2015. Over-approximating loops to prove properties using bounded model checking. In: Proceedings of Design, Automation and Test in Europe Conference and Exhibition, DATE. Grenoble, France, pp. 1407\u20131412.","DOI":"10.7873\/DATE.2015.0245"},{"key":"10.1016\/j.jss.2023.111897_b9","doi-asserted-by":"crossref","unstructured":"Dutta, S., 2022. Localizing Faults Using Verification Technique. In: Proceedings of Innovations in Software Engineering Conference, ISEC. pp. 1\u201311.","DOI":"10.1145\/3511430.3511445"},{"issue":"4","key":"10.1016\/j.jss.2023.111897_b10","doi-asserted-by":"crossref","first-page":"1267","DOI":"10.1109\/TR.2019.2956120","article-title":"Hierarchically localizing software faults using DNN","volume":"69","author":"Dutta","year":"2019","journal-title":"IEEE Trans. Reliab."},{"issue":"4","key":"10.1016\/j.jss.2023.111897_b11","doi-asserted-by":"crossref","first-page":"1267","DOI":"10.1109\/TR.2019.2956120","article-title":"Hierarchically localizing software faults using DNN","volume":"69","author":"Dutta","year":"2020","journal-title":"IEEE Trans. Reliab."},{"issue":"1","key":"10.1016\/j.jss.2023.111897_b12","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0004-3702(99)00034-X","article-title":"Model-based diagnosis of hardware designs","volume":"111","author":"Friedrich","year":"1999","journal-title":"Artificial Intelligence"},{"issue":"4","key":"10.1016\/j.jss.2023.111897_b13","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/j.entcs.2006.12.032","article-title":"Automated fault localization for C programs","volume":"174","author":"Griesmayer","year":"2007","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"10.1016\/j.jss.2023.111897_b14","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1002\/stvr.421","article-title":"Fault localization using a model checker","volume":"20","author":"Grismayer","year":"2010","journal-title":"Softw. Test. Verif. Reliab."},{"key":"10.1016\/j.jss.2023.111897_b15","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10009-005-0202-0","article-title":"Error explanation with distance metrics","volume":"8","author":"Groce","year":"2006","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.jss.2023.111897_b16","doi-asserted-by":"crossref","unstructured":"Groce, A., Kroening, D., Lerda, F., 2004. Understanding Counterexamples with explain. In: Computer Aided Verification (CAV). Berlin, Heidelberg, pp. 453\u2013456.","DOI":"10.1007\/978-3-540-27813-9_35"},{"key":"10.1016\/j.jss.2023.111897_b17","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W., 2003. What Went Wrong: Explaining Counterexamples. In: Proceedings of International SPIN Workshop on Model Checking of Software. Berlin, Heidelberg, pp. 121\u2013136.","DOI":"10.1007\/3-540-44829-2_8"},{"issue":"2","key":"10.1016\/j.jss.2023.111897_b18","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1109\/TCAD.2003.822105","article-title":"Using global code motions to improve the quality of results for high-level synthesis","volume":"23","author":"Gupta","year":"2004","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"10.1016\/j.jss.2023.111897_b19","unstructured":"Hutchins, M., Foster, H., Goradia, T., Ostrand, T., 1994. Experiments on the effectiveness of dataflow- and control-flow-based test adequacy criteria. In: Proceedings of 16th International Conference on Software Engineering, ICSE. Sorrento, Italy, pp. 191\u2013200."},{"key":"10.1016\/j.jss.2023.111897_b20","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar: Cause Clue Clauses, R., 2011. Error Localization Using Maximum Satisfiability. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. San Jose, California, USA, pp. 437\u2013446.","DOI":"10.1145\/1993498.1993550"},{"issue":"3","key":"10.1016\/j.jss.2023.111897_b21","doi-asserted-by":"crossref","first-page":"556","DOI":"10.1109\/TCAD.2007.913390","article-title":"An equivalence-checking method for scheduling verification in high-level synthesis","volume":"27","author":"Karfa","year":"2008","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"10.1016\/j.jss.2023.111897_b22","unstructured":"Lattner, C., Adve, V., 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: Proceedings of the International Symposium on Code Generation and Optimization, CGO. San Jose, CA, USA."},{"issue":"3","key":"10.1016\/j.jss.2023.111897_b23","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/S0022-0000(71)80035-1","article-title":"Mathematical theory of partial correctness","volume":"5","author":"Manna","year":"1971","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/j.jss.2023.111897_b24","unstructured":"Mayer, W., Abreu, R., Stumptner, M., Gemund, A.J.C., 2008. Prioritizing Model-Based Debugging Diagnostic Reports. In: Procedings of the 19th International Workshop on Principles of Diagnosis. pp. 127\u2013134."},{"year":"2003","series-title":"Model-based debugging using multiple abstract models","author":"Mayer","key":"10.1016\/j.jss.2023.111897_b25"},{"key":"10.1016\/j.jss.2023.111897_b26","unstructured":"Mayer, W., Stumptner, M., 2007. Abstract Interpretation of Programs for Model-Based Debugging. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, IJCAI. Hyderabad, India, pp. 471\u2013476."},{"key":"10.1016\/j.jss.2023.111897_b27","unstructured":"Mayer, W., Stumptner, M., Wieland, D., Wotawa, F., 2002. Towards an Integrated Debugging Environment. In: Proceedings of the 15th Eureopean Conference on Artificial Intelligence, ECAI. Lyon, France, pp. 422\u2013426."},{"key":"10.1016\/j.jss.2023.111897_b28","unstructured":"Renieres, M., Reiss, S.P., 2003. Fault localization with nearest neighbor queries. In: International Conference on Automated Software Engineering, Montreal. Canada, pp. 30\u201339."},{"key":"10.1016\/j.jss.2023.111897_b29","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip","year":"1995","journal-title":"J. Program. Lang."},{"key":"10.1016\/j.jss.2023.111897_b30","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","article-title":"Program slicing","author":"Weiser","year":"1984","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.jss.2023.111897_b31","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J., 2011. Finding and understanding bugs in C compilers. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. San Jose, CA, USA, pp. 283\u2013284.","DOI":"10.1145\/1993498.1993532"},{"key":"10.1016\/j.jss.2023.111897_b32","unstructured":"Zaks, A., Pnueli, A., 2008. CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In: Proceedings of International Symposium on Formal Methods, FM. Turku, Finland."}],"container-title":["Journal of Systems and Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121223002923?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121223002923?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T23:36:35Z","timestamp":1759016195000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0164121223002923"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3]]},"references-count":32,"alternative-id":["S0164121223002923"],"URL":"https:\/\/doi.org\/10.1016\/j.jss.2023.111897","relation":{},"ISSN":["0164-1212"],"issn-type":[{"type":"print","value":"0164-1212"}],"subject":[],"published":{"date-parts":[[2024,3]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Localizing faults using verification technique","name":"articletitle","label":"Article Title"},{"value":"Journal of Systems and Software","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jss.2023.111897","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2023 Elsevier Inc. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"111897"}}