Mostly-automated verification of low-level programs in computational separation logic.

Adam Chlipala

Browse the full PLDI paper archive.