Brittany Nkounkou
PhD 2020 & MS 2016, Computer Science, Cornell University
BSE 2012, Computer Science and Engineering, University of Connecticut
NSF Graduate Research Fellow, 2012
Alfred P. Sloan Graduate Scholar, 2012
n k o u n k o u (a) c s . c o r n e l l . e d u
Dissertation
Certified Software for Designing Asynchronous Circuits August 2020 [pdf] [code]
Committee: Ross Tate, Rajit Manohar, Hakim Weatherspoon, Bob Constable
I used Coq to mechanically formalize the semantics of CHP (Communicating Hardware Processes, a high-level language used to design asynchronous circuits) and build a certified CHP simulator.
Publication
Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications PLDI 2015 [downloads]
Authors: Stephen Longfield, Brittany Nkounkou, Rajit Manohar, Ross Tate
I used Coq to mechanically prove that our newly developed CHP semantics used in our CHP-error-detection tool are equivalent to the commonly accepted CHP semantics.