VLDB 2026 Research / reviewers in the wild / expert
Patricia Firlejczyk
dblp:426/2520
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2025
0009-0001-8916-329XORCID · 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 · 87% Programming languages and type systems · 13% |
Topics — the 3 heaviest of 3, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program verification
modular verification |
0.9 | 1 | 2025 | Modular Reasoning about Global Variables and Their Initialization · Proc. ACM Program. Lang. 2025 |
Program verification › program logic
separation logic |
0.9 | 1 | 2025 | Modular Reasoning about Global Variables and Their Initialization · Proc. ACM Program. Lang. 2025 |
Programming languages and type systems
module systems |
0.3 | 1 | 2025 | Modular Reasoning about Global Variables and Their Initialization · Proc. ACM Program. Lang. 2025 |
Methods — techniques the papers use, named apart from their topics
separation logic · 0.9rocq · 0.9iris · 0.9
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Modular Reasoning about Global Variables and Their InitializationabstractMany imperative programming languages offer global variables to implement common functionality such as global caches and counters. Global variables are typically initialized by module initializers (e.g., static initializers in Java), code blocks that are executed automatically by the runtime system. When or in what order these initializers run is typically not known statically and modularly. For instance in Java, initialization is triggered dynamically upon the first use of a class, while in Go, the order depends on all packages of a program. As a result, reasoning modularly about global variables and their initialization is difficult, especially because module initializers may perform arbitrary side effects and may have cyclic dependencies. Consequently, existing modular verification techniques either do not support global state or impose drastic restrictions that are not satisfied by mainstream languages and programs. In this paper, we present the first practical verification technique to reason formally and modularly about global state and its initialization. Our technique is based on separation logic and uses module invariants to specify ownership and values of global variables. A partial order on modules and methods allows us to reason modularly about when a module invariant may be soundly assumed to hold, irrespective of when exactly the module initializer establishing it runs. Our technique supports both thread-local and shared global state. We formalize it as a program logic in Iris and prove its soundness in Rocq. We make only minimal assumptions about the initialization semantics, making our technique applicable to a wide range of programming languages. We implemented our technique in existing verifiers for Java and Go and demonstrate its effectiveness on typical uses cases of global state as well as a substantial codebase implementing an Internet router. João C. Pereira, Isaac van Bakel, Patricia Firlejczyk, Marco Eilers, Peter Müller 0001 |
Proc. ACM Program. Lang. | 3 |