A Rewriting Logic Approach to Type Inference. - Chucky Ellison; Traian-Florin Serbanuta; Grigore Rosu (WADT, 2008)

Matching Logic: An Alternative to Hoare/Floyd Logic. - Grigore Rosu; Chucky Ellison; Wolfram Schulte (AMAST, 2010)

The K Primer (version 3.3). - Traian-Florin Serbanuta; Andrei Arusoaie; David Lazar; Chucky Ellison; Dorel Lucanu; Grigore Rosu (K, 2011)

Executing Formal Semantics with the K Tool. - David Lazar; Andrei Arusoaie; Traian-Florin Serbanuta; Chucky Ellison; Radu Mereuta; Dorel Lucanu; Grigore Rosu (FM, 2012)

Test-case reduction for C compiler bugs. - John Regehr; Yang Chen 024; Pascal Cuoq; Eric Eide; Chucky Ellison; Xuejun Yang (PLDI, 2012)

An executable formal semantics of C with applications. - Chucky Ellison; Grigore Rosu (POPL, 2012)

Making Maude Definitions More Interactive. - Andrei Arusoaie; Traian-Florin Serbanuta; Chucky Ellison; Grigore Rosu (WRLA, 2012)

A formal semantics of C with applications - Chucky Ellison (2012)

Defining the undefinedness of C. - Chris Hathhorn; Chucky Ellison; Grigore Rosu (PLDI, 2015)