Nathan Chong

I am a Principal Applied Scientist for AWS in the Automated Reasoning Group. I help programmers write better programs and architects design better systems. I enjoy working at many levels of the system stack, but particularly verification and specification at the hardware/software boundary.

I got my PhD at Imperial College London with Alastair F. Donaldson on scalable verification techniques for data-parallel programs.

Awards

• 2022: Most influential OOPSLA paper
• 2018: PLDI Distinguished Paper Award
• 2015: EPSRC Doctoral Prize Fellowship
• 2014: EPSRC ICT Pioneers

Talks and Drafts

• [pdf][video][proofs] FreeRTOS meets separation logic: memory safety, thread safety and functional correctness proofs in VeriFast,   CAV'20 Sponsored Event (23 July 2020)
• [talk][video] The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++,   PLDI'18 (20 June 2018)
• [pdf] Reasoning about Transactional Memory, Axiomatically,   FMATS-5 (21 Sept 2017)

Work

• [pdf] Anthony C.J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, Nathan Chong A Verification Methodology for Arm Confidential Compute Architecture,   ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2023
• [pdf] Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, Adrian Sampson Verifying Dynamic Trait Objects in Rust,   International Conference on Software Engineering (Software Engineering in Practice), 2022
• [pdf][video][proofs] Nathan Chong, Bart Jacobs Formally Verifying the FreeRTOS IPC Mechanism,   Embedded World Conference, 2021
• [pdf][related blog part 1, part 2] Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle Code-Level Model Checking in the Software Development Workflow,   International Conference on Software Engineering (Software Engineering in Practice), 2020
• [pdf][artifact][talk][video][blog part 1, part 2] Nathan Chong, Tyler Sorensen, John Wickerson The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++,   ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018 (Distinguished Paper Award)
• [pdf] Adam Betts, Nathan Chong, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema Implementing and Evaluating Candidate-Based Invariant Generation,   IEEE Transactions on Software Engineering, 2017
• Alastair F. Donaldson, Ganesh Gopalakrishnan, Nathan Chong, Jeroen Ketema, Guodong Li, Peng Li, Anton Lokhmotov, Shaz Qadeer Formal Analysis Techniques for Reliable GPU Programming: Current Solutions and Call to Action,   Book chapter in Advances in GPU Research and Practice, pp. 3-21 (Morgan Kaufmann), 2017
• [pdf] Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, John Wickerson The Design and Implementation of a Verification Technique for GPU Kernels,   ACM Transactions on Programming Languages and Systems, 2015
• [pdf][artifact] Christopher Lidbury, Andrei Lascu, Nathan Chong, Alastair F. Donaldson Many-Core Compiler Fuzzing,   ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015
• [pdf][artifact] Nathan Chong Scalable Verification Techniques for Data-Parallel Programs,   Imperial College London (PhD thesis), 2014
• [pdf][artifact] Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Daniel Liew, Shaz Qadeer Engineering a Static Verification Tool for GPU Kernels,   Computer Aided Verification, 2014
• [pdf][artifact] Nathan Chong, Alastair F. Donaldson, Jeroen Ketema A Sound and Complete Abstraction for Reasoning about Parallel Prefix Sums,   ACM SIGPLAN Symposium on Principles of Programming Languages, 2014
• [pdf][artifact] Nathan Chong, Alastair F. Donaldson, Paul H.J. Kelly, Jeroen Ketema, Shaz Qadeer Barrier Invariants: a Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels,   ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2013
• [pdf] Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, Paul Thomson GPUVerify: a Verifier for GPU Kernels,   ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2012
• Nathan Chong, Emre Ozer, Krisztián Flautner IP Modeling and Verification,   Book chapter in Processor and System-on-Chip Simulation (Springer), 2010