{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:09:31Z","timestamp":1784196571279,"version":"3.55.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Pattern matching is a powerful mechanism for writing safe and expressive conditional logic. Once primarily associated with functional programming, it has become a common paradigm even in non-functional languages, such as Java. Languages that support pattern matching include specific analyzers, known as pattern-match coverage analyzers, to ensure its correct and efficient use by statically verifying properties such as exhaustiveness and redundancy. However, these analyzers can suffer from soundness and completeness issues, leading to false negatives (unsafe patterns mistakenly accepted) or false positives (valid patterns incorrectly rejected).<\/jats:p>\n                  <jats:p>In this work, we present a systematic approach for validating soundness and completeness in pattern-match coverage analyzers. The approach consists of a novel generator for algebraic data types and pattern-matching statements, supporting features that increase the complexity of coverage analysis, such as generalized algebraic data types. To establish the test oracle without building a reference implementation from scratch, the approach generates both exhaustive and inexhaustive pattern-matching cases, either by construction or by encoding them as SMT formulas. The latter leads to a universal test oracle that cross-checks coverage analysis results against a constraint solver, exposing soundness and completeness bugs in case of inconsistencies.<\/jats:p>\n                  <jats:p>\n                    We implement this approach in\n                    <jats:sc>Ikaros<\/jats:sc>\n                    , which we evaluate on three major compilers: Scala, Java, and Haskell. Despite pattern-match coverage analyzers being only a small part of these compilers, Ikaros has uncovered 16 bugs, of which 12 have been fixed. Notably, 7 instances were important soundness bugs that could lead to unexpected runtime errors. Additionally, Ikaros provides a scalable framework for extending it to any language with ML-like pattern matching.\n                  <\/jats:p>","DOI":"10.1145\/3763171","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"3371-3397","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Validating Soundness and Completeness in Pattern-Match Coverage Analyzers"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-3847-1088","authenticated-orcid":false,"given":"Cyril Flurin","family":"Moser","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9906-3073","authenticated-orcid":false,"given":"Thodoris","family":"Sotiropoulos","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7285-289X","authenticated-orcid":false,"given":"Chengyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2970-1391","authenticated-orcid":false,"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485500"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523427"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363562"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689746"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351266"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.04.002"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.65"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598130"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1795772"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632919"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Jacques Garrigue and Jacques Le Normand. 2017. GADTs and Exhaustiveness: Looking for the Impossible. arXiv e-prints Article arXiv:1702.02281 (Feb. 2017) arXiv:1702.02281 pages. arXiv:1702.02281 [cs.PL] doi:10.48550\/arXiv.1702.02281","DOI":"10.48550\/arXiv.1702.02281"},{"key":"e_1_3_1_15_1","unstructured":"Jacques Garrigue and JL Normand. 2011. Adding GADTs to OCaml: the direct approach. In Workshop on ML. 27."},{"key":"e_1_3_1_16_1","unstructured":"James Gosling Bill Joy Guy Steele Gilad Bracha Alex Buckley Daniel Smith and Gavin Bierman. 2024. The Java Language Specification: Java SE 22 Edition. https:\/\/docs.oracle.com\/javase\/specs\/jls\/se22\/jls22.pdf."},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408989"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547653"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462194"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858949.2784748"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547622"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480927"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"issue":"1","key":"e_1_3_1_24_1","first-page":"100","article-title":"Differential Testing for Software","volume":"10","author":"McKeeman William M.","year":"1998","unstructured":"William M. McKeeman. 1998. Differential Testing for Software. Digit. Tech. J. 10, 1 (1998), 100\u2013107. http:\/\/dblp.uni-trier.de\/db\/journals\/dtj\/dtj10.html#McKeeman98","journal-title":"Digit. Tech. J"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134307"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Cyril Moser Thodoris Sotiropoulos Chengyu Zhang and Zhendong Su. 2025. Artifact for \u201cValidating Soundness and Completeness in Pattern-Match Coverage Analyzers\u201d. doi:10.5281\/zenodo.16909625","DOI":"10.5281\/zenodo.16909625"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_1_29_1","unstructured":"Rust Team. 2025. Pattern and Exhaustiveness Checking. https:\/\/rustc-dev-guide.rust-lang.org\/pat-exhaustive-checking.html. Online accessed; 19-03-2025."},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632904"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628161"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/25.4.465"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689795"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604150"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586048"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763171","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:01:45Z","timestamp":1784196105000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763171"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":38,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763171"],"URL":"https:\/\/doi.org\/10.1145\/3763171","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}