Qinxiang Cao



  • Undergraduate Students: (1) projects about algorithm verification and/or (2) projects about smart contract verification. Pick an algorithm or a smart contract, prove its correctness and efficiency, FORMALLY. 

  • Masters & Doctoral Students: projects about logics for program verification. The general theories of how to prove programs correct. 
    Feel free to contact me if you have any questions.



  • Ph.D. 2013-2018: Computer Science, Princeton University (Advisor: Andrew W.Appel)

  • Bachelor 2009-2013: Logic, Department of Philosophy, Peking University

  • Bachelor 2010-2013: Math (double major), Department of Math, Peking University 

  • High School 2006-2009: Shanghai High School


  • "Talk is cheap. Show me the proof." ---Qinxiang Cao

Research Interests

Algorithm correctness verification, program verification, program semantics, separation logic, concurrent program verification.

Selected Publications
  • VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs, Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds and Andrew W. Appel. Journal of Automatic Reasoning (JAR) 2018. 

  • Proof pearl: Magic wand as frame, by Qinxiang Cao, Shengyi Wang, Aquinas Hobor, and Andrew W. Appel, February 2018. 

  • Bringing Order to the Separation Logic Jungle, Qinxiang Cao, Santiago Cuellar, Andrew W. Appel. In Asian Symposium on Programming Language and Systems (APLAS) 2017. 

  • On Axiomatizations of Public Announcement Logic, Yanjing Wang and Qinxiang Cao. In Synthes 190 (2013): 190, 103–134. 

  • Verifiable C. Fifth Volumn of Software Foundation. Andrew W. Appel and Qinxiang Cao. (In preparation)

Honors and Awards
  • 1st place of NOI 2008 (National Olympiads in Informatics) 

  • 1st place of CMO 2009 (China Mathematics Competition) 

  • Committee of CTSC 2011 (China Team Selection Contest for IOI) 

  • Committee of NOI 2011 (National Olympiads in Informatics) 

© John Hopcroft Center, Shanghai Jiao Tong University