Modular Verification of Intrusive List and Tree Data Structures in Separation Logic.

Marc Hermes, Robbert Krebbers

Browse the full ITP paper archive.