Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification

Christoph Sprenger, Tobias Klenze, Marco Eilers +4

Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation bet…