Zhaozhong Ni

3PAR Inc.
Email: nzz@acm.org
Tel/Fax: (425)793-4221

Previously, I was at Programming Languages and Methods Group of Microsoft Research. Before that, I was in the FLINT project and obtained my PhD degree from Department of Computer Science, Yale University.

About Me

Curriculum Vitae: pdf

Publications

Automating Separation-Logic Verification with General-Purpose First-Order Theorem Prover (draft).
Zhaozhong Ni. Technical Report. August 2009
An Abstract, Approximation-Based Approach to Embedded Code Pointers and Partial-Correctness (implementation).
Zhaozhong Ni. Technical Report. August 2008
Supporting Unrestricted Recursive Types.
Zhaozhong Ni. Technical Report. October 2007
Using XCAP to Certify Realistic System Code: Machine Context Management.
Zhaozhong Ni, Dachuan Yu, and Zhong Shao.
In Proc. 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'07), Kaiserslautern, Germany, pages 189-206, September 2007.
An Open Framework for Foundational Proof-Carrying Code.
Xinyu Feng, Zhaozhong Ni, Zhong Shao, and Yu Guo.
In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07), Nice, France, pages 67-78, January 2007.
A Translation from Typed Assembly Languages to Certified Assembly Programming.
Zhaozhong Ni and Zhong Shao. Technical Report. October 2006
Modular Verification of Machine-Level Thread Implementation..
Zhaozhong Ni, Dachuan Yu, and Zhong Shao. Technical Report. November 2006
Modular Verification of Assembly Code with Stack-Based Control Abstractions.
Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni.
In Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), Ottawa, Canada, pages 401-414, June 2006.
Certified Assembly Programming with Embedded Code Pointers.
Zhaozhong Ni and Zhong Shao.
In Proc. 33rd ACM Symposium on Principles of Programming Languages (POPL'06), Charleston, South Carolina, pages 320-333, January 2006.
A Syntactic Approach to Foundational Proof-Carrying Code (Extended Version).
Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni.
Journal of Automated Reasoning (Special Issue on Proof-Carrying Code) 31 (3-4): 191-229, 2003.
A Syntactic Approach to Foundational Proof-Carrying Code.
Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni.
In Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), Copenhagen, Denmark, pages 89-100, July 2002.
An Encoding of Fomega in LF.
Carsten Schürmann, Dachuan Yu, and Zhaozhong Ni.
In Proc. 2001 Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'01), Siena, Italy, June 2001.