| 2013 | PLDI | Formal verification of SSA-based optimizations for LLVM. | Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic |
| 2012 | CPP | Mechanized Verification of Computing Dominators for Formalizing Compilers. | Jianzhou Zhao, Steve Zdancewic |
| 2012 | POPL | Formalizing the LLVM intermediate representation for verified program transformations. | Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic |
| 2010 | APLAS | Relational Parametricity for a Polymorphic Linear Lambda Calculus. | Jianzhou Zhao, Qi Zhang, Steve Zdancewic |
| 2010 | POPL | Dependent types and program equivalence. | Limin Jia, Jianzhou Zhao, Vilhelm Sjberg, Stephanie Weirich |
| 2009 | PLDI | SoftBound: highly compatible and complete spatial memory safety for c. | Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic |
| 2008 | ICFP | AURA: a programming language for authorization and audit. | Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic |
| 2005 | CSCWD | Cooperation of SMV and Jeda for the property checking of mixed control and data intensive designs. | Jianzhou Zhao, Jinian Bian, Weimin Wu |
| 2004 | COMPSAC | PFGASAT- A Genetic SAT Solver Combining Partitioning and Fuzzy Strategie. | Jianzhou Zhao, Jinian Bian, Weimin Wu |