{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:59:46Z","timestamp":1743015586800,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031720437"},{"type":"electronic","value":"9783031720444"}],"license":[{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"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":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-72044-4_2","type":"book-chapter","created":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:02:41Z","timestamp":1725897761000},"page":"25-44","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Is MCDC Really Better? Lessons from\u00a0Combining Tests and\u00a0Proofs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2051-1494","authenticated-orcid":false,"given":"Li","family":"Huang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5985-7434","authenticated-orcid":false,"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[]},{"given":"Manuel","family":"Oriol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,10]]},"reference":[{"key":"2_CR1","volume-title":"Introduction to Software Testing","author":"P Ammann","year":"2017","unstructured":"Ammann, P., Offutt, J.: Introduction to Software Testing, 2nd edn. Cambridge University Press, Cambridge (2017)","edition":"2"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Ammann, P., Offutt, J., Huang, H.: Coverage criteria for logical expressions. In: 2003 14th International Symposium on Software Reliability Engineering, ISSRE 2003, pp. 99\u2013107. IEEE (2003)","DOI":"10.1109\/ISSRE.2003.1251034"},{"key":"2_CR3","unstructured":"AutoProof. http:\/\/autoproof.sit.org\/"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Awedikian, Z., Ayari, K., Antoniol, G.: MC\/DC automatic test input data generation. In: Proceedings of the 11th Annual Conference on Genetic and Evolutionary Computation, pp. 1657\u20131664 (2009)","DOI":"10.1145\/1569901.1570123"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects. Lecture Notes in Computer Science, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11804192_17"},{"issue":"3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1241572.1241581","volume":"32","author":"PV Bhansali","year":"2007","unstructured":"Bhansali, P.V.: The MCDC paradox. ACM SIGSOFT Softw. Eng. Notes 32(3), 1\u20134 (2007)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-31762-0_2","volume-title":"Formal Verification of Object-Oriented Software","author":"T Bormer","year":"2012","unstructured":"Bormer, T., et al.: The COST IC0701 verification competition 2011. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 3\u201321. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31762-0_2"},{"key":"2_CR8","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: Constraint reasoning in FocalTest. In: ICSOFT (2010)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Chilenski, J., Miller, S.P.: Applicability of modified condition\/decision coverage to software testing. Softw. Eng. J. 9, 193\u2013200 (1994). https:\/\/api.semanticscholar.org\/CorpusID:27283960","DOI":"10.1049\/sej.1994.0025"},{"issue":"5","key":"2_CR10","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1049\/sej.1994.0025","volume":"9","author":"JJ Chilenski","year":"1994","unstructured":"Chilenski, J.J., Miller, S.P.: Applicability of modified condition\/decision coverage to software testing. Softw. Eng. J. 9(5), 193\u2013200 (1994)","journal-title":"Softw. Eng. J."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Ciupa, I., Leitner, A., Oriol, M., Meyer, B.: Experimental assessment of random testing for object-oriented software. In: Proceedings of the 2007 International Symposium on Software Testing and Analysis, pp. 84\u201394 (2007)","DOI":"10.1145\/1273463.1273476"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Ciupa, I., Leitner, A., Oriol, M., Meyer, B.: ARTOO: adaptive random testing for object-oriented software. In: International Conference on Software Engineering (ICSE), p. 71\u201380 (2008)","DOI":"10.1145\/1368088.1368099"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"2_CR14","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall (1976)"},{"key":"2_CR15","unstructured":"DO-178B: Software considerations in airborne systems and equipment certification (1992)"},{"key":"2_CR16","unstructured":"DO-178C: Software considerations in airborne systems and equipment certification (2011)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Dupuy, A., Leveson, N.: An empirical evaluation of the MC\/DC coverage criterion on the HETE-2 satellite software. In: IEEE DASC: Digital Aviation Systems Conference, pp. 1B6\/1\u20131B6\/7 (2000)","DOI":"10.1109\/DASC.2000.886883"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Dutta, A., Kumar, S., Godboley, S.: Enhancing test cases generated by concolic testing. In: Proceedings of the 12th Innovations on Software Engineering Conference (formerly known as India Software Engineering Conference), pp. 1\u201311 (2019)","DOI":"10.1145\/3299771.3299781"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Huang, L., Meyer, B.: A failed proof can yield a useful test. arXiv:2208.09873 (2022)","DOI":"10.1002\/stvr.1859"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Huang, L., Meyer, B., Oriol, M.: Improving counterexample quality from failed program verification. In: International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 268\u2013273. IEEE (2022)","DOI":"10.1109\/ISSREW55968.2022.00078"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-031-43240-8_4","volume-title":"Testing Software and Systems","author":"L Huang","year":"2023","unstructured":"Huang, L., Meyer, B., Oriol, M.: Seeding contradiction: a fast method for generating full-coverage test suites. In: Bonfanti, S., Gargantini, A., Salvaneschi, P. (eds.) ICTSS 2023. LNCS, vol. 14131, pp. 52\u201370. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43240-8_4"},{"key":"2_CR22","unstructured":"International Electrotechnical Commission (IEC): IEC 61508-3:2010 - Functional safety of electrical\/electronic\/programmable electronic safety-related systems - Part 3: Software requirements (see Functional Safety and IEC 61508) (2010)"},{"key":"2_CR23","unstructured":"International Organization for Standardization (ISO): ISO 26262-3:2011 - Road vehicles \u2014 Functional safety (2011)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Just, R., Jalali, D., Inozemtseva, L., Ernst, M.D., Holmes, R., Fraser, G.: Are mutants a valid substitute for real faults in software testing? In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 654\u2013665 (2014)","DOI":"10.1145\/2635868.2635929"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-99130-6_9","volume-title":"Computer Safety, Reliability, and Security","author":"T Kitamura","year":"2018","unstructured":"Kitamura, T., Maissonneuve, Q., Choi, E.-H., Artho, C., Gargantini, A.: Optimal test suite generation for modified condition decision coverage using SAT solving. In: Gallina, B., Skavhaug, A., Bitsch, F. (eds.) SAFECOMP 2018. LNCS, vol. 11093, pp. 123\u2013138. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99130-6_9"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V Klebanov","year":"2011","unstructured":"Klebanov, V., et al.: The 1st verified software competition: experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154\u2013168. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_14"},{"key":"2_CR27","unstructured":"Leino, K.R.M.: Program Proofs. MIT Press (2023)"},{"key":"2_CR28","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: The Boogie 2 type system: design and verification condition generation. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.146.4277"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Marcozzi, M., Bardin, S., Delahaye, M., Kosmatov, N., Prevosto, V.: Taming coverage criteria heterogeneity with LTest. In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST), pp. 500\u2013507. IEEE (2017)","DOI":"10.1109\/ICST.2017.57"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Meyer, B.: Applying \u201cdesign by contract.\u201d Computer 25(10), 40\u201351 (1992)","DOI":"10.1109\/2.161279"},{"key":"2_CR31","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall (1997)"},{"key":"2_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92145-5","volume-title":"Touch of Class: Learning to Program Well with Objects and Contracts","author":"B Meyer","year":"2016","unstructured":"Meyer, B.: Touch of Class: Learning to Program Well with Objects and Contracts. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-540-92145-5"},{"key":"2_CR33","unstructured":"Mustafin, I., Schena, A., Weber, R.: buggy-java-jml-eiffel (2024). https:\/\/github.com\/CI-CSE\/buggy-java-jml-eiffel"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Nilizadeh, A., Leavens, G.T., Le, X.B.D., P\u0103s\u0103reanu, C.S., Cok, D.R.: Exploring true test overfitting in dynamic automated program repair using formal methods. In: 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST), pp. 229\u2013240. IEEE (2021)","DOI":"10.1109\/ICST49551.2021.00033"},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Paul, T.K., Lau, M.F.: A systematic literature review on modified condition and decision coverage. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC 2014, pp. 1301\u20131308. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2554850.2555004","DOI":"10.1145\/2554850.2555004"},{"key":"2_CR36","unstructured":"Radio Technical Commission for Aeronautics (RTCA): RTCA\/DO-178B Software Considerations in Airborne Systems and Equipment Certification (1992)"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Rani, G.M., Godboley, S.: Poster: a gCov based new profiler, gMCov, for MC\/DC and SC-MCC. In: 2022 IEEE Conference on Software Testing, Verification and Validation (ICST), pp. 469\u2013472 (2022https:\/\/doi.org\/10.1109\/ICST53961.2022.00058","DOI":"10.1109\/ICST53961.2022.00058"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Rayadurgam, S., Heimdahl, M.P.E.: Coverage based test-case generation using model checkers. In: Proceedings. Eighth Annual IEEE International Conference and Workshop On the Engineering of Computer-Based Systems-ECBS 2001, pp. 83\u201391. IEEE (2001)","DOI":"10.1109\/ECBS.2001.922409"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013white box test generation for .NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134\u2013153. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-79124-9_10"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-662-46681-0_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Tschannen","year":"2015","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566\u2013580. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_53"},{"key":"2_CR41","unstructured":"US Department of Transportation: An Investigation of Three Forms of the Modified Condition Decision Coverage (MCDC) Criterion, final report, DOT\/FAA\/AR-01\/18 (2001)"},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-45648-1_15","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"SA Vilkomir","year":"2002","unstructured":"Vilkomir, S.A., Bowen, J.P.: Reinforced condition\/decision coverage (RC\/DC): a new criterion for software testing. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 291\u2013308. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45648-1_15"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-87873-5_10","volume-title":"Verified Software: Theories, Tools, Experiments","author":"BW Weide","year":"2008","unstructured":"Weide, B.W., et al.: Incremental benchmarks for software verification tools and techniques. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 84\u201398. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87873-5_10"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Yang, L., Yan, J., Zhang, J.: Generating minimal test set satisfying MC\/DC criterion via sat based approach. In: ACM Symposium on Applied Computing, pp. 1899\u20131906 (2018)","DOI":"10.1145\/3167132.3167335"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-72044-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:05:13Z","timestamp":1725897913000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-72044-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,10]]},"ISBN":["9783031720437","9783031720444"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-72044-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,10]]},"assertion":[{"value":"10 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","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":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}