Modular Reasoning about Global Variables and Their Initialization

Explore a groundbreaking conference presentation that introduces the first practical verification technique for formally and modularly reasoning about global state and its initialization in imperative programming languages. Learn how researchers from ETH Zurich have developed a novel approach using separation logic and module invariants to address the longstanding challenge of verifying programs with global variables, which are commonly used for implementing global caches, counters, and other shared functionality. Discover how this technique handles the complex problem of module initializers that execute automatically but with unpredictable timing and ordering, such as static initializers in Java that trigger upon first class use or Go's package-dependent initialization order. Understand the innovative use of a partial order on modules and methods that enables modular reasoning about when module invariants can be safely assumed to hold, regardless of the exact execution timing of module initializers. Examine how the approach supports both thread-local and shared global state while making minimal assumptions about initialization semantics, making it applicable across a wide range of programming languages. See the practical implementation of this technique in existing verifiers for Java and Go, demonstrated through typical global state use cases and a substantial Internet router codebase, with formal soundness proofs developed in Iris and verified in Rocq.