Thesis: Certified Software for Developing Asynchronous Hardware
Committee: Ross Tate, Rajit Manohar, Hakim Weatherspoon, Bob Constable


I am currently using Coq to mechanically specify and verify program transformations in Communicating Hardware Processes (CHP), a language used to develop asynchronous circuits.

Stephen Longfield, Brittany Nkounkou, Rajit Manohar, Ross Tate. Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications. PLDI 2015 [paper] [code]

Post-Silicon Validation Test Coverage and Simulation of TrueNorth. IBM Research. Summer 2015