Local Reasoning for Reconfigurable Distributed Systems
Published in RWTH Aachen University (Bachelor Thesis), 2021
This Bachelor thesis presents a framework for reasoning about dynamically reconfigurable distributed systems modeled in the DR-BIP framework. It develops a separation logic tailored to BIP configurations and introduces a reconfiguration language to express structural changes in distributed systems. The logic enables formal verification of reconfiguration programs using Hoare-style inference rules and a generalized frame rule, combining static and dynamic reasoning with havoc semantics. The approach is demonstrated through correctness proofs for reconfiguration programs on parametric token rings.
Recommended citation: Emma Ahrens: "Local Reasoning for Reconfigurable Distributed Systems." Bachelor Thesis, RWTH Aachen University, March 5, 2021.
Download Paper | Download Slides