EDBT 2026 Demo / reviewers in the wild / expert
Yalun Liang
dblp:375/1004
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2025
0009-0002-1943-8662ORCID · 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 |
Compilers and program optimization · 67% Concurrent programming · 33% |
Topics — the 3 heaviest of 3, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Compilers and program optimization › compiler construction
compositional compilation |
0.9 | 1 | 2025 | CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks · Proc. ACM Program. Lang. 2025 |
Concurrent programming › concurrency models › multithreading
multithreaded programs |
0.9 | 1 | 2025 | CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks · Proc. ACM Program. Lang. 2025 |
Compilers and program optimization
verified compilation |
0.9 | 1 | 2025 | CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks · Proc. ACM Program. Lang. 2025 |
Methods — techniques the papers use, named apart from their topics
kripke memory relations · 0.9coq · 0.9
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared StacksabstractIt is a long-standing open problem to support verified compilation of multi-threaded programs compositionally when sharing of stack data between threads is allowed. Although certain solutions exist on paper, none of them is completely formalized because of the difficulty in simultaneously enabling sharing and forbidding modification of stack memory in presence of arbitrary memory operations (e.g., pointer arithmetic). We present a compiler verification framework that solves this open problem in the setting of cooperative multi-threading. To address the challenges of sharing stack data, we introduce threaded Kripke memory relations (TKMR) to support both protection and sharing of stacks in a multi-stack memory model. We further introduce threaded forward simulations parameterized by TKMR to capture semantics preservation for compiling program modules in multi-threaded contexts. We show that threaded forward simulations are both horizontally composable— thereby enabling the compositional verification of open threads and heterogeneous modules—and vertically composable— thereby enabling composition of compiler correctness for multiple compiler passes. Furthermore, threaded forward simulations can be converted into backward simulations. We apply this framework to 18 passes of CompCert to get CompCertOC, the first optimizing verified compiler that supports compositional verification of cooperative multi-threaded programs with shared stacks. Ling Zhang 0012, Yuting Wang 0001, Yalun Liang, Zhong Shao 0001 |
Proc. ACM Program. Lang. | 3 |