Separation Logic for Small-step Cminor

Andrew W. Appel, Sandrine Blazy

Cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to Cminor and from Cminor to machine language. We have redesigned Cminor…