EDBT 2026 Demo / reviewers in the wild / expert
Andrés Lomelí Garduño
dblp:425/5357
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2026
0009-0005-8922-790XORCID · reported
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 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 · 61% Concurrent programming · 39% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program verification
concurrent program verification |
1.0 | 1 | 2026 | Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models · Proc. ACM Program. Lang. 2026 |
Program verification › termination analysis
non-termination proving |
1.0 | 1 | 2026 | Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models · Proc. ACM Program. Lang. 2026 |
Concurrent programming › memory models
weak memory models |
1.0 | 1 | 2026 | Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models · Proc. ACM Program. Lang. 2026 |
Concurrent programming
memory models |
0.3 | 1 | 2026 | Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models · Proc. ACM Program. Lang. 2026 |
Methods — techniques the papers use, named apart from their topics
recurrence sets · 1.0lasso-finding algorithm · 1.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency ModelsabstractRecurrence sets characterize non-termination in sequential programs. We present a generalization of recurrence sets to concurrent programs that run on weak memory models. Sequential programs have operational semantics in terms of states and transitions, and classical recurrence sets are defined as sets of states that are existentially closed under transitions. Concurrent programs have axiomatic semantics in terms of executions, and our new recurrence sets are defined as sets of executions that are existentially closed under extensions. The semantics of concurrent programs is not only affected by the memory model, but also by fairness assumptions about its environment, be it the scheduler or the memory subsystems. Our new recurrence sets are formulated relative to such fairness assumptions. We show that our recurrence sets are sound for proving fair non-termination on all practical memory models, and even complete on many. To turn our theory into practice, we develop a new automated technique for proving fair non-termination in concurrent programs on weak memory models. At the heart of this technique is a finite representation of recurrence sets in terms of execution-based lassos. We implemented a lasso-finding algorithm in Dartagnan, and evaluated it on a number of programs running under CPU and GPU memory models. Thomas Haas 0001, Roland Meyer 0001, Hernán Ponce de León, Andrés Lomelí Garduño |
Proc. ACM Program. Lang. | 4 |