Zhaozhong Ni Programming Languages and Methods Group Microsoft Research Email: nzz@acm.org Tel: (425)793-4221 Fax: (425)793-4221

About Me

• Curriculum Vitae: pdf

• Research Statement: pdf

Publications

• Automating Separation-Logic Verification with General-Purpose First-Order Theorem Prover (draft).
  Zhaozhong Ni. Technical Report. January 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 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.