Siyuan He

I'm currently a Ph.D. student in computer science at Purdue University in West Lafayette, and my research advisor is Tiark Rompf. My research area is programming language (functional programming) and formal verification (especially Coq and VST).

Currently, I'm active to potential internship opportunities and research collaboration.

Though not mentioned in the research section, I have a very wide range of research interest because of my various research experience. I have several experience in machine learning, including NLP, time series and especially CV and causal inference. I also tried cryptography for a very short term before I switched to programming language and formal verification.

My current work focus on formal verification of a web server implemented by C language. I'm also working in a programming language group to develop a programming language. However, many of my knowledge and strategies on programming language are derived from my experience in formal verification, which is not a well-satisfied a shortcut. In the following steps, I will switch more to programming language side.


  • Purdue University, West Lafayette
  • Computer Science

2021 -

  • University of Michigan, Ann Arbor
  • Science in Information

2019 - 2021

  • Shanghai Jiaotong University, Shanghai
  • Electrical and Computer Engineering

2016 - 2020


Teaching Assistant
  • Shanghai Jiaotong University, Shanghai
  • VE370: Computer Organization

2019 Summer

Research Experience

Formal verification of a path-finding algorithm

University of Michigan, Advisor: Prof. Jean-Baptiste Jeannin

  • Develop a path-finding algorithm to find path under ATC command in airport.
  • Formally write all the specifications and prove the correctness in Coq.
  • Write the paper and present.

November 2020 - August 2021

Extraction to OCaml, Hazel

University of Michigan - Future of Programming Lab, Advisor: Prof. Cyrus Omar.

  • Working on the extraction from Hazel code to OCaml code. The extraction will explicitly fully-annotate all variables with type. Exception messages will be thrown on the cases of extraction failure, such as unsupported syntax. Formalize part of the extraction rules.

December 2019 - present


University of Illinois at Chicago, Advisor: Prof. William Mansky.

  • Adding concurrency feature to the deepweb, working on proofs now.

August 2020 - present


    Verification of an Airport Taxiway Path-Finding Algorithm. Siyuan He, Ke Du, Joshua Wilhelm and Jean-Baptiste Jeannin. In Digital Aerospace Systems Conference (DASC 2020), to appear.


University of Michigan - Future of Programming Lab

Directed by Prof. Cyrus Omar.

  • Implement the extraction from Hazel code to OCaml code
  • Formalize part of the extraction rules from static syntax to OCaml Code.

December 2019 - present

Assessing Humor in Edited News Headlines

SI630 Course Project & Online Competition

Build a NLP model to predict the level of humor of a editing operation that replace one word in a newspaper headline. The most innovative point is encoding the editing action into a vector representation, which is a new topic with almost no research or reference.

February 2020 - April 2020

Temperature Forecasting

Master Capstone Design

Propose a model to forecast the temperature of a certain place, which involves time series forecasting. Our model features deep learning based model and extra features, which beats some common models.

February 2021 - April 2021

Anomaly Detection in Injection Molding

Bachelor Capstone Design

Propose a model to detect anomaly in the injection molding process of industrial plastic production. The project is sponsored by Foxconn.

May 2020 - August 2020


SJTU VE370 Course Project

Use Verilog to implement a MIPS pipeline CPU to support basic instructions.

February 2019 - May 2019

Search engine on games

UM SI650 Course Project

Implemented a domain-specific search engine, featuring static ranking, filter on dislike, pseudo relevance feed-back, spell correction and query suggestion.

2019 Fall

Multivariate Cryptography

SJTU VE475 Course Project

Overview and implement the multivariate cryptography structure. Provide a simple proof for the NP-hardness of the MQ problem.

2019 Summer

Clustering based on potential and repulsion

SJTU VE488 Course Project || Further Research

Introduce the repulsion and potential in physics to clustering method. Develop and implement a fast clustering approximation method.

2018 Summer

Intern Experience

Computer Vision Researcher

Lenovo AI-Lab, Beijing

  • Develop a blur detection method and optimize the pre-processing efficiency.
  • Optimize the align performance and overall recall of the face recognition model.

December 2017 - February 2018

Data Analysis

Nokia Shanghai-Bell, Shanghai

  • Involved in smart street-lamp network project, complete all lab tests and find problems.
  • Involved in the design of frontend and backend of a smart education system.
  • Develop an automation program to take over manual work in daily form filling.

May 2020 - August 2020