Lambda the Ultimate

An Executable Formal Semantics of C with Applications
Chucky Ellison & Grigore Rosu, POPL '12

This paper describes an executable formal semantics of C. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes 99.2% of 776 test programs. It is the most complete and thoroughly tested formal definition of C to date. The semantics yields an interpreter, debugger, state space search tool, and model checker “for free”. The semantics is shown capable of automatically finding program errors, both statically and at runtime. It is also used to enumerate nondeterministic behavior.

This is the most ambitious use of rewriting logic that I've yet seen. On its face it seems like a quite elegant and general-purpose formulation; this specific C semantics is open sourced, even.

For more background I recommend the main page on the K framework.

Anyone else investigating this system and style of semantics definition?