EDBT 2026 Demo / reviewers in the wild / expert
Cyril Moser
dblp:419/7789
· DBLP profile ↗
1ranked-venue papers
1as first author
1since 2021 · last 2025
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 1 first-author · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
1 paper |
Software testing · 38% Program verification · 38% Programming languages and type systems · 23% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Software testing
compiler testing |
0.9 | 1 | 2025 | Validating Soundness and Completeness in Pattern-Match Coverage Analyzers · Proc. ACM Program. Lang. 2025 |
Program verification
SMT-based verification |
0.9 | 1 | 2025 | Validating Soundness and Completeness in Pattern-Match Coverage Analyzers · Proc. ACM Program. Lang. 2025 |
Programming languages and type systems › functional programming
algebraic data types |
0.3 | 1 | 2025 | Validating Soundness and Completeness in Pattern-Match Coverage Analyzers · Proc. ACM Program. Lang. 2025 |
Programming languages and type systems › control structures
pattern matching |
0.3 | 1 | 2025 | Validating Soundness and Completeness in Pattern-Match Coverage Analyzers · Proc. ACM Program. Lang. 2025 |
Methods — techniques the papers use, named apart from their topics
test generation · 0.9SMT solving · 0.9
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Validating Soundness and Completeness in Pattern-Match Coverage AnalyzersabstractPattern 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). 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. We implement this approach in Ikaros , 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. Cyril Moser, Thodoris Sotiropoulos, Chengyu Zhang 0001, Zhendong Su 0001 |
Proc. ACM Program. Lang. | 1 |