{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T09:13:17Z","timestamp":1769764397264,"version":"3.49.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Debugging is one of the most time-consuming and expensive tasks in software development. Several formula-based fault localization (FBFL) methods have been proposed, but they fail to guarantee a set of diagnoses across all failing tests or may produce redundant diagnoses that are not subset-minimal, particularly for programs with multiple faults.<\/jats:p><jats:p>This paper introduces a novel fault localization approach for C programs with multiple faults. <jats:sc>CFaults<\/jats:sc> leverages Model-Based Diagnosis (MBD) with multiple observations and aggregates all failing test cases into a unified MaxSAT formula. Consequently, our method guarantees consistency across observations and simplifies the fault localization procedure. Experimental results on two benchmark sets of C programs, <jats:sc>TCAS<\/jats:sc> and <jats:sc>C-Pack-IPAs<\/jats:sc>, show that <jats:sc>CFaults<\/jats:sc> is faster than other FBFL approaches like <jats:sc>BugAssist<\/jats:sc> and <jats:sc>SNIPER<\/jats:sc>. Moreover, <jats:sc>CFaults<\/jats:sc> only generates subset-minimal diagnoses of faulty statements, whereas the other approaches tend to enumerate redundant diagnoses.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_24","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"463-481","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["cfaults: Model-Based Diagnosis for\u00a0Fault Localization in\u00a0C with\u00a0Multiple Test Cases"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7407-5967","authenticated-orcid":false,"given":"Pedro","family":"Orvalho","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3487-784X","authenticated-orcid":false,"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4205-2189","authenticated-orcid":false,"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"Abreu, R., Zoeteweij, P., van Gemund, A.J.C.: Spectrum-based multiple fault localization. In: ASE 2009, 24th IEEE\/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, November 16-20 2009, pp. 88\u201399. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/ASE.2009.25","DOI":"10.1109\/ASE.2009.25"},{"issue":"11","key":"24_CR2","doi-asserted-by":"publisher","first-page":"1780","DOI":"10.1016\/J.JSS.2009.06.035","volume":"82","author":"R Abreu","year":"2009","unstructured":"Abreu, R., Zoeteweij, P., Golsteijn, R., van Gemund, A.J.C.: A practical evaluation of spectrum-based fault localization. J. Syst. Softw. 82(11), 1780\u20131792 (2009). https:\/\/doi.org\/10.1016\/J.JSS.2009.06.035","journal-title":"J. Syst. Softw."},{"key":"24_CR3","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"24_CR4","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model checking, 2nd Edition. MIT Press (2018). https:\/\/mitpress.mit.edu\/books\/model-checking-second-edition"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"24_CR6","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods Syst. Des. 25(2\u20133), 105\u2013127 (2004). https:\/\/doi.org\/10.1023\/B:FORM.0000040025.89719.F3","DOI":"10.1023\/B:FORM.0000040025.89719.F3"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570\u2013574. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_40"},{"key":"24_CR8","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: Proceedings of the 40th Design Automation Conference, DAC 2003, Anaheim, CA, USA, 2-6 June 2003, pp. 368\u2013371. ACM (2003). https:\/\/doi.org\/10.1145\/775832.775928","DOI":"10.1145\/775832.775928"},{"issue":"4","key":"24_CR9","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991). https:\/\/doi.org\/10.1145\/115372.115320","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"24_CR10","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."},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15-17 June 2015, pp. 229\u2013239 (2015)","DOI":"10.1145\/2737924.2737977"},{"key":"24_CR12","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.) Proceedings of the Workshop on Verification and Debugging, V &D@FLoC 2006, Seattle, WA, USA, 21 August 2006. Electronic Notes in Theoretical Computer Science, 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":"3","key":"24_CR13","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1109\/54.785838","volume":"16","author":"MC Hansen","year":"1999","unstructured":"Hansen, M.C., Yalcin, H., Hayes, J.P.: Unveiling the ISCAS-85 benchmarks: a case study in reverse engineering. IEEE Des. Test Comput. 16(3), 72\u201380 (1999). https:\/\/doi.org\/10.1109\/54.785838","journal-title":"IEEE Des. Test Comput."},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-319-94144-8_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Ignatiev","year":"2018","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a Python toolkit for prototyping with SAT oracles. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 428\u2013437. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_26"},{"issue":"1","key":"24_CR15","first-page":"53","volume":"11","author":"A Ignatiev","year":"2019","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: an efficient MaxSAT solver. J. Satisf. Boolean Model. Comput. 11(1), 53\u201364 (2019)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Ignatiev, A., Morgado, A., Weissenbacher, G., Marques-Silva, J.: Model-based diagnosis with multiple observations. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, 10-16 August 2019, pp. 1108\u20131115. (2019). https:\/\/doi.org\/10.24963\/IJCAI.2019\/155, https:\/\/www.ijcai.org\/","DOI":"10.24963\/IJCAI.2019\/155"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-22110-1_40","volume-title":"Computer Aided Verification","author":"M Jose","year":"2011","unstructured":"Jose, M., Majumdar, R.: Bug-Assist: assisting fault localization in ANSI-C programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 504\u2013509. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_40"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 437\u2013446. ACM (2011)","DOI":"10.1145\/1993498.1993550"},{"key":"24_CR19","unstructured":"K\u00f6nighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: Bjesse, P., Slobodov\u00e1, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, Austin, TX, USA, October 30 - November 02, 2011, pp. 91\u2013100. FMCAD Inc. (2011). http:\/\/dl.acm.org\/citation.cfm?id=2157671"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-11737-9_17","volume-title":"Formal Methods and Software Engineering","author":"S-M Lamraoui","year":"2014","unstructured":"Lamraoui, S.-M., Nakajima, S.: A formula-based approach for automatic fault localization of imperative programs. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 251\u2013266. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11737-9_17"},{"issue":"1","key":"24_CR21","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."},{"issue":"1","key":"24_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/S10817-007-9084-Z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1\u201333 (2008). https:\/\/doi.org\/10.1007\/S10817-007-9084-Z","journal-title":"J. Autom. Reason."},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Liu, K., Koyuncu, A., Bissyand\u00e9, T.F., Kim, D., Klein, J., Le\u00a0Traon, Y.: You cannot fix what you cannot find! an investigation of fault localization bias in benchmarking automated program repair systems. In: 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST), pp. 102\u2013113. IEEE (2019)","DOI":"10.1109\/ICST.2019.00020"},{"key":"24_CR24","unstructured":"Marques-Silva, J., Janota, M., Ignatiev, A., Morgado, A.: Efficient model based diagnosis with maximum satisfiability. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25-31 July 2015, pp. 1966\u20131972. AAAI Press (2015). http:\/\/ijcai.org\/Abstract\/15\/279"},{"key":"24_CR25","doi-asserted-by":"publisher","unstructured":"Metodi, A., Stern, R., Kalech, M., Codish, M.: A novel sat-based approach to model based diagnosis. J. Artif. Intell. Res. 51, 377\u2013411 (2014). https:\/\/doi.org\/10.1613\/JAIR.4503","DOI":"10.1613\/JAIR.4503"},{"key":"24_CR26","doi-asserted-by":"publisher","unstructured":"Naish, L., Lee, H.J., Ramamohanarao, K.: A model for spectra-based software diagnosis. ACM Trans. Softw. Eng. Methodol. 20(3), 11:1\u201311:32 (2011). https:\/\/doi.org\/10.1145\/2000791.2000795","DOI":"10.1145\/2000791.2000795"},{"key":"24_CR27","doi-asserted-by":"publisher","unstructured":"Orvalho, P., Janota, M., Manquinho, V.: C-Pack of IPAs: a C90 program benchmark of introductory programming assignments. CoRR abs\/2206.08768 (2022). https:\/\/doi.org\/10.48550\/arXiv.2206.08768","DOI":"10.48550\/arXiv.2206.08768"},{"key":"24_CR28","doi-asserted-by":"publisher","unstructured":"Orvalho, P., Janota, M., Manquinho, V.: MultIPAs: applying program transformations to introductory programming assignments for data augmentation. In: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2022, pp. 1657\u20131661. ACM, Singapore (2022). https:\/\/doi.org\/10.1145\/3540250.3558931","DOI":"10.1145\/3540250.3558931"},{"key":"24_CR29","doi-asserted-by":"publisher","unstructured":"Orvalho, P., Janota, M., Manquinho, V.: C-Pack of IPAs: a C90 program benchmark of introductory programming assignments. In: International Workshop on Automated Program Repair, APR@ICSE 2024, Lisbon, Portugal, April 20, 2024, pp.\u00a0\u2013 (2024). https:\/\/doi.org\/10.1145\/3643788.3648010","DOI":"10.1145\/3643788.3648010"},{"key":"24_CR30","doi-asserted-by":"publisher","unstructured":"Orvalho, P., Janota, M., Manquinho, V.: CFaults: model-based diagnosis for fault localization in C with multiple test cases (2024). https:\/\/doi.org\/10.5281\/zenodo.12510220, https:\/\/github.com\/pmorvalho\/CFaults","DOI":"10.5281\/zenodo.12510220"},{"key":"24_CR31","doi-asserted-by":"publisher","unstructured":"Orvalho, P., Janota, M., Manquinho, V.: InvAASTCluster: on applying invariant-based program clustering to introductory programming assignments (2022). https:\/\/doi.org\/10.48550\/ARXIV.2206.14175, https:\/\/arxiv.org\/abs\/2206.14175","DOI":"10.48550\/ARXIV.2206.14175"},{"key":"24_CR32","doi-asserted-by":"publisher","unstructured":"Orvalho, P., Piepenbrock, J., Janota, M., Manquinho, V.M.: Graph neural networks for mapping variables between programs. In: ECAI 2023 - 26th European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol.\u00a0372, pp. 1811\u20131818. IOS Press, Poland (2023). https:\/\/doi.org\/10.3233\/FAIA230468","DOI":"10.3233\/FAIA230468"},{"key":"24_CR33","unstructured":"pycparser (2024). https:\/\/github.com\/eliben\/pycparser. Accessed 18 April 2024"},{"issue":"1","key":"24_CR34","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":"24_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-030-53291-8_33","volume-title":"Computer Aided Verification","author":"B-C Rothenberg","year":"2020","unstructured":"Rothenberg, B.-C., Grumberg, O.: Must fault localization for program repair. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 658\u2013680. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_33"},{"key":"24_CR36","doi-asserted-by":"publisher","unstructured":"Safarpour, S., Mangassarian, H., Veneris, A.G., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, 11-14 November 2007, Proceedings, pp. 13\u201319. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/FAMCAD.2007.26","DOI":"10.1109\/FAMCAD.2007.26"},{"issue":"3","key":"24_CR37","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/S10664-020-09931-7","volume":"26","author":"EO Soremekun","year":"2021","unstructured":"Soremekun, E.O., Kirschner, L., B\u00f6hme, M., Zeller, A.: Locating faults with program slicing: an empirical analysis. Empir. Softw. Eng. 26(3), 51 (2021). https:\/\/doi.org\/10.1007\/S10664-020-09931-7","journal-title":"Empir. Softw. Eng."},{"issue":"2","key":"24_CR38","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/J.JSS.2009.09.037","volume":"83","author":"WE Wong","year":"2010","unstructured":"Wong, W.E., Debroy, V., Choi, B.: A family of code coverage-based heuristics for effective fault localization. J. Syst. Softw. 83(2), 188\u2013208 (2010). https:\/\/doi.org\/10.1016\/J.JSS.2009.09.037","journal-title":"J. Syst. Softw."},{"issue":"1","key":"24_CR39","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1109\/TR.2013.2285319","volume":"63","author":"WE Wong","year":"2014","unstructured":"Wong, W.E., Debroy, V., Gao, R., Li, Y.: The Dstar method for effective software fault localization. IEEE Trans. Reliab. 63(1), 290\u2013308 (2014). https:\/\/doi.org\/10.1109\/TR.2013.2285319","journal-title":"IEEE Trans. Reliab."},{"issue":"8","key":"24_CR40","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1109\/TSE.2016.2521368","volume":"42","author":"WE Wong","year":"2016","unstructured":"Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F.: A survey on software fault localization. IEEE Trans. Software Eng. 42(8), 707\u2013740 (2016). https:\/\/doi.org\/10.1109\/TSE.2016.2521368","journal-title":"IEEE Trans. Software Eng."},{"issue":"4","key":"24_CR41","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.: Automated debugging based on a constraint model of the program and a test case. J. Log. Algebraic Methods Program 81(4), 390\u2013407 (2012). https:\/\/doi.org\/10.1016\/J.JLAP.2012.03.002","journal-title":"J. Log. Algebraic Methods Program"},{"key":"24_CR42","doi-asserted-by":"publisher","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using Boolean satisfiability. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, 12-14 January 2005, pp. 351\u2013363. ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040334","DOI":"10.1145\/1040305.1040334"},{"key":"24_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48166-4_16","volume-title":"Software Engineering \u2014 ESEC\/FSE \u201999","author":"A Zeller","year":"1999","unstructured":"Zeller, A.: Yesterday, my program worked. today, it does not. why? In: Nierstrasz, O., Lemoine, M. (eds.) ESEC\/SIGSOFT FSE -1999. LNCS, vol. 1687, pp. 253\u2013267. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48166-4_16"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:07:01Z","timestamp":1725934021000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}