EDBT 2026 Demo / reviewers in the wild / expert
Romit Roy Chowdhury
dblp:390/3684
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2024
0009-0004-4097-8115ORCID · 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 |
Concurrent programming · 75% Program verification · 25% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Concurrent programming › atomicity
linearizability |
0.8 | 1 | 2024 | Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Proc. ACM Program. Lang. 2024 |
Concurrent programming
memory models |
0.8 | 1 | 2024 | Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Proc. ACM Program. Lang. 2024 |
Program verification › neural network verification
robustness verification |
0.8 | 1 | 2024 | Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Proc. ACM Program. Lang. 2024 |
Concurrent programming › memory models
weak memory models |
0.8 | 1 | 2024 | Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Proc. ACM Program. Lang. 2024 |
Methods — techniques the papers use, named apart from their topics
non-robustness witness search · 0.8inductive verification · 0.8
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2024 | Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsabstractClients reason about the behavior of concurrent data structure libraries such as sets, queues, or stacks using specifications that capture well-understood correctness conditions, such as linearizability. The implementation of these libraries, however, focused as they are on performance, may additionally exploit relaxed memory behavior allowed by the language or underlying hardware that weaken the strong ordering and visibility constraints on shared-memory accesses that would otherwise be imposed by a sequentially consistent (SC) memory model. As an alternative to developing new specification and verification mechanisms for reasoning about libraries under relaxed memory model, we instead consider the orthogonal problem of library robustness , a property that holds when all possible behaviors of a library implementation under relaxed memory model are also possible under SC. In this paper, we develop a new automated technique for verifying robustness of library implementations in the context of a C11-style memory model. This task is challenging because a most-general client may invoke an unbounded number of concurrently executing library operations that can manipulate an unbounded number of shared locations. We establish a novel inductive technique for verifying library robustness that leverages prior work on the robustness problem for the C11 memory model based on the search for a non-robustness witness under SC executions. We crucially rely on the fact that this search is carried out over SC executions, and use high-level SC specifications (including linearizability) of the library to verify the absence of a non-robustness witness. Our technique is compositional - we show how we can safely preserve robustness of multiple interacting library implementations and clients using additional SC fences to guarantee robustness of entire executions. Experimental results on a number of complex realistic library implementations demonstrate the feasibility of our approach. Kartik Nagar, Anmol Sahoo, Romit Roy Chowdhury, Suresh Jagannathan |
Proc. ACM Program. Lang. | 3 |