An executable formal semantics of C with applications.

Chucky Ellison, Grigore Rosu

Browse the full POPL paper archive.