My picture

He Zhu

Assistant Professor
Computer Science Department
Rutgers University, New Brunswick
Email: hz375@cs.rutgers.edu


[Awards] [Research] [Teaching] [Publications] [Service]
I am looking for motivated PhD and undergraduate students to join the RU Automated Reasoning group!
Please drop me an email with your CV if you are interested. Application deadline is Jan. 1st. 2021 for PhD students.

I am an assistant professor in the Department of Computer Science at Rutgers University-New Brunswick. My research is under the broad umbrella of automated reasoning and formal methods, focusing on improving the safety and provable correctness of programming systems via program analysis, program verification, program synthesis, and machine learning.

My current interest lies at the intersection of deep learning and symbolic (program) reasoning. I am investigating how to make deep learning systems, especially deep reinforcement learning systems, more data-efficient, reliable, and trustworthy.

I obtained my Ph.D. from Purdue CS, advised by Suresh Jagannathan.

News

  • NSF Grant: Formal Symbolic Reasoning of Deep Reinforcement Learning Systems!
  • DARPA Grant: Symbiotic Design for Cyber Physical Systems!

  • Awards

  • ACM SIGPLAN PLDI 2019 Distinguished Paper Award.
  • ACM SIGPLAN PLDI 2018 Distinguished Paper Award.
  • Maurice H. Halstead Memorial Award (Purdue University).

  • Research

    My research generally falls into the areas of programming languages, formal methods, and machine learning. My current research is primarily centered around how to integrate formal program reasoning techniques, such as program synthesis and program verification, into reinforcement learning training loops. My long-term research goal is to build intelligent and explainable neural-symbolic systems that allow the tight integration of deep learning and symbolic reasoning and that can be formally certified correct and reliable.

    Teaching

  • CS 314. Principles of Programming Languages [S21]
  • CS 515. Programming Languages and Compilers [F20]
  • CS 314. Principles of Programming Languages [S20]
  • CS 515. Programming Languages and Compilers [F19]

  • Publications

    ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks [pdf]
    Xuankang Lin, He Zhu, Roopsha Samanta and Suresh Jagannathan.
    Formal Methods in Computer-Aided Design (FMCAD), 2020

    An Inductive Synthesis Framework for Verifiable Reinforcement Learning [pdf][code]
    ACM SIGPLAN distinguished paper award
    He Zhu, Zikang Xiong, Stephen Magill and Suresh Jagannathan
    Proceedings of the 40th ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), 2019

    A Data-Driven CHC Solver [pdf][code]
    ACM SIGPLAN distinguished paper award
    He Zhu, Stephen Magill and Suresh Jagannathan
    Proceedings of the 39th ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), 2018

    Automatically Learning Shape Specifications [pdf][code]
    He Zhu, Gustavo Petri and Suresh Jagannathan
    Proceedings of the 37th ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), 2016

    Learning Refinement Types [pdf][code]
    He Zhu, Aditya V. Nori and Suresh Jagannathan
    Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2015

    Poling: SMT Aided Linearizability Proofs [pdf]
    He Zhu, Gustavo Petri and Suresh Jagannathan
    Proceedings of the 27th International Conference on Computer Aided Verification (CAV), 2015

    Dependent Array Type Inference from Tests [pdf]
    He Zhu, Aditya V. Nori and Suresh Jagannathan
    Proceedings of the 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015

    Compositional and Lightweight Dependent Type Inference for ML [pdf]
    He Zhu and Suresh Jagannathan
    Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013


    Service

  • 2021: PLDI PC
  • 2020: CAV AEC co-chair, CAV PC, NSF Panelist, TSE Reviewer
  • 2019: HCVS PC