headshot

Nathan Chong

I am a final year PhD student interested in scalable verification techniques for data-parallel programs. My research interests are parallel programming, computer architecture and formal reasoning. Specifications and problems at the hardware/software boundary get me excited. My previous work in this area include proofs of correctness for cache-coherence protocols, memory models and formalising architectural specifications. Currently, I am very interested in the formal semantics of GPU programs and automatically proving good properties about them. Accelerators are increasingly common and I don’t believe formal methods and verification techniques have caught up with programming them.

I have a background in industry as a research engineer at ARM where I worked on hardware and software at many levels of the system stack.

ICT Pioneers, June 2014

I was very fortunate to take part in the EPSRC ICT Pioneers 2014 competition. The core message of my talk was about the need and opportunity for static verification to provide powerful tools to help programmers write better programs. For more information about GPUVerify check out our main webpage and these introductory tutorials and videos.

Tools

I am a key contributor to GPUVerify, a verification technique and tool for the automatic analysis of GPU kernels written in OpenCL and CUDA. At ARM I developed prototypes and tools for CPU virtualisation (now found in the ARMv7 architecture), cache coherence verification (now in AMBA4 ACE) and instruction set simulators (the Cortex-M1 simulator shipped in RVDS).

I am an advocate of repeatable and reproducible research that enables other researchers to build upon my work. The accompanying artifact to my OOPSLA'12 paper was approved by the OOPSLA evaluation committee and allows others to use GPUVerify and repeat the experimental evaluation given in my paper. I recently served on the PLDI 2014 artifact evaluation committee. I am also currently serving on the POPL 2015 artifact evaluation committee.

Papers