# Chucky Ellison

From K Framework

Chucky Ellison is a former grad student from the University of Illinois at Urbana-Champaign working with prof. Grigore Rosu. He graduated in 2012.

His new website can be found here: http://www.freefour.com/.

**Role in the K Framework Project**

- Working on the semantics of C.
- Gave formal semantics to a number of esoteric languages including BF and Befunge.
- Involved in the Matching Logic project.

## Publications Related to the K Framework

*A Formal Semantics of C with Applications*- Chucky Ellison
, University of Illinois, July 2012**PhD Thesis**

PDF, Slides, Project, BIB *Executing Formal Semantics with the K Tool*- David Lazar, Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu and Grigore Rosu
, LNCS 7436, pp 267-271. 2012**FM'12**

PDF, Slides(PDF), FM'12, DBLP, BIB *Defining the Undefinedness of C*- Chucky Ellison and Grigore Rosu
http://hdl.handle.net/2142/30780, April 2012**Technical Report**

PDF, TR@UIUC, BIB *Test-Case Reduction for C Compiler Bugs*- John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison and Xuejun Yang
, ACM, pp 335-346. 2012**PLDI'12**

PDF, Slides(PPT), Project, ACM, PLDI'12, DBLP, BIB *The K Primer (version 2.5)*- Traian Florin Serbanuta, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu and Grigore Rosu
, January 2012**Technical Report**

PDF, K 2.5, BIB *Making Maude Definitions more Interactive*- Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison and Grigore Rosu
, LNCS 7571. 2012**WRLA'12**

PDF, Slides (PDF), WRLA'12, BIB *An Executable Formal Semantics of C with Applications*- Chucky Ellison and Grigore Rosu
, ACM, pp 533-544. 2012**POPL'12**

PDF, Slides(PDF), Project, ACM, POPL'12, DBLP, BIB *On Compiling Rewriting Logic Language Definitions into Competitive Interpreters*- Michael Ilseman, Chucky Ellison and Grigore Rosu
http://hdl.handle.net/2142/17444, December 2010**Technical Report**

PDF, TR@UIUC, Compiler Webpage, BIB *Matching Logic: An Alternative to Hoare/Floyd Logic*- Grigore Rosu, Chucky Ellison and Wolfram Schulte
, LNCS 6486, pp 142-162. 2010**AMAST'10**

PDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB *A Rewriting Logic Approach to Type Inference*- Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
, LNCS 5486, pp 135-151. 2009**WADT'08**

PDF, Slides(PDF), LNCS, WADT'08, BIB *From Rewriting Logic Executable Semantics to Matching Logic Program Verification*- Grigore Rosu, Chucky Ellison and Wolfram Schulte
http://hdl.handle.net/2142/13159, July 2009**Technical Report**

PDF, TR@UIUC, BIB *A Rewriting Logic Approach to Defining Type Systems*- Chucky Ellison
**Master's Thesis**

PDF, TR@UIUC, BIB *A Rewriting Logic Approach to Type Inference*- Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
UIUCDCS-R-2008-2934, March 2008**Technical report**

PDF, TR@UIUC, BIB