Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle.

Viorel Preoteasa

Browse the full IFM paper archive.