Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data.

Andrés Lomelí Garduño

dblp:425/5357 · DBLP profile ↗
← Back
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

TopicWeightPapersLastEvidence papers
Program verification
concurrent program verification
1.012026
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.012026
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.012026
Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models · Proc. ACM Program. Lang. 2026
Concurrent programming
memory models
0.312026
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
YearPublicationVenuePosition
2026 Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
abstract
Recurrence 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