EDBT 2026 Demo / reviewers in the wild / expert
Jerome Jochems
dblp:300/8943
· DBLP profile ↗
1ranked-venue papers
1as first author
1since 2021 · last 2023
0000-0002-3853-9277ORCID · reported
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 |
Program verification · 100% | |
| Theoretical computer science
1 paper |
Logic in computer science · 100% |
Topics — the 2 heaviest of 3, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program verification
higher-order program verification |
0.7 | 1 | 2023 | Higher-Order MSL Horn Constraints · Proc. ACM Program. Lang. 2023 |
Program verification › model checking
higher-order recursion schemes |
0.7 | 1 | 2023 | Higher-Order MSL Horn Constraints · Proc. ACM Program. Lang. 2023 |
Methods — techniques the papers use, named apart from their topics
resolution-based decision procedure · 1.3
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2023 | Higher-Order MSL Horn ConstraintsabstractThe monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which make them well suited to higher-order program verification. In fact, we show that the higher-order MSL satisfiability problem and the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to verified socket programming. Jerome Jochems, Eddie Jones, Steven Ramsay |
Proc. ACM Program. Lang. | 1 |