Yuantian Ding

I’m Yuantian Ding, a 4th-year PhD student at Purdue University specializing in program synthesis and verification under the supervision of Prof. Xiaokang Qiu.

Education

Purdue University (2022 - Present)
Ph.D. Electrical and Computer Engineering
Advised by Xiaokang Qiu

University of Science and Technology of China (2018 - 2022)
B.E. in Computer Science and Technology
GPA: 3.97/4.3 (Ranked 6/251)

Publication

Enhanced Enumeration of Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations.
Yuantian Ding, Xiaokang Qiu.
(POPL ’24) Proc. 51st ACM SIGPLAN Symposium on Principles of Programming Languages.
PDF DOI CODE TALK SLIDES LINK

A Concurrent Approach to String Transformation Synthesis.
Yuantian Ding, Xiaokang Qiu.
(PLDI ’25) Proc. 46th ACM SIGPLAN Conference on Programming Language Design and Implementation.
PDF DOI CODE TALK SLIDES

Experience

Nanjing University Research Internship (07/2021 - 12/2021)
with Zhiqiang Zuo, Harry Xu
Topic: A New Serverless Platform with Customized JIT Design

SRI SSFT24: The 13th Summer School on Formal Techniques (07/2021 - 12/2021)
Summer school for learning techniques based on formal logic.

Projects

DryadSynth: Dryad Synthesizer for SyGuS competition
A SyGuS solver designed by Purdue CAP, under active development.
SITE CODE

Awards

ASC Student Supercomputer Challenge 2021 First Prize
Topic (My Part): Efficient Parallelization of PRESTO

ACM-China International Parallel Computing Challenge 2020 Third Prize
Topic (Final): Efficient Numerical Simulation of Supersonic Underexpanded Thermal Jets

Old Projects

Oomotion A textobject-oriented editor plugin for VS Code
A editing keymap inspired by Vim, Kakoune and Helix. Able to edit code based on text-objects like words, lines, code blocks, etc. With tree-sitter and easy-motion support.
SITE CODE

TheoryComboViz Polite theory combination visualizer
A visualizer for polite theory combination, demonstrated using Sets, intended to make SMT solvers easier to understand.
SLIDES CODE DEMO

HilbertProver A prover for Hilbert system
An Automatic Theorem Prover for Hilbert System, generating nearly-minimal proofs, with some interesting optimizations.
DEMO CODE

Chital A secure container runtime implemented in Rust
Course project for my operating system course. Leading 3 other students in a group.
PDF CODE

Project Notes

A New Serverless Platform with Customized JIT Design

Faas (Function as a service) is one form of serverless computing where users only need to deploy function on the cloud and the cloud service vendor will handle all the hardware resources the function needs. The vendor will provide runtimes for these functions which are driven by events. However, Faas is tailored for short-lived functions which makes traditional runtime optimizations such as JIT compilation fail to enhance performance. We want to design a new framework to bridge the gap between modern language runtime and serverless platforms.

In this project, we aim at building a new serverless platform tailored for JVM runtime with profile information sharing and native code sharing across nodes. We also hope to use hardware tracing technology to help reduce profiling overhead from interpreter stage.

I stopped working on this after working with Xiaokang. Here is the previous status: Implementation Report.