I study Certified Software for Developing Asynchronous Hardware with Ross Tate and Rajit Manohar as an Exchange Scholar in the Computer Systems Lab at Yale University.


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] [artifact]

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