Zhaozhong Ni

I am a Researcher in the Programming Languages and Methods Group, Microsoft Research. Some of my current and future work are also related to the Singularity Project.

About Me

• Email: zhaozhong.ni@microsoft.com

• Telephone: (425)421-7499

• Fax: (425)936-7329

• Address: Microsoft Research, One Microsoft Way, Redmond, WA 98052 USA

• Curriculum Vitae: (pdf, html, txt)

Publications

• An Abstract, Approximation-Based Approach to Embedded Code Pointers and Partial-Correctness. Coq code
  Zhaozhong Ni. Technical Report.

• A Translation from Typed Assembly Languages to Certified Assembly Programming.
  Zhaozhong Ni and Zhong Shao. Technical Report.

• Using XCAP to Certify Realistic System Code: Machine Context Management..
  Zhaozhong Ni, Dachuann 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.

• 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.

Education

My Ph.D. study was done in the FLINT Project led by Professor Zhong Shao, at Department of Computer Science, Yale University. My dissertation, Modular Machine Code Verification, was defined in November, 2006.