Jianlin Herman Li
Phd Student
Cheriton School of Computer Science, University of Waterloo
                 

I am a Ph.D. student in the Programming Languages Group at the University of Waterloo (since Fall 2021), co-supervised by Yizhou Zhang and Ondřej Lhoták.

I care about software safety and efficiency across the entire life cycle: from design (model checking), to program (program analysis, and formal verification via automatic and interactive theorem proving such as Rocq, Agda, and Lean), to compilation (type checking, optimization, and compiler correctness).

I design probabilistic programming languages and implement compilers for sound and scalable (Bayesian) inference. My work applies type systems, program analyses, and logical relations to achieve efficient, reliable, and certified probabilistic programming.

Previously, I worked on formal verification of adversarial robustness of deep neural networks.

I am currently seeking both academic and industrial positions.[CV]

Peer-Reviewed Publications (while at the University of Waterloo)
    ICFP 2025
Compiling with Generating Functions

Geni: A compiler that compiles functional-programming-style probabilistic programs into probability-generating functions, a compact and exact compilation target representing measures.

Jianlin Li, Yizhou Zhang

Acceptance rate: 32.73%, 36 accepted out of 110 submissions

[ DOI | Artifact | TR | Talk ]

    PLDI 2024
Compiling Probabilistic Programs for Variable Elimination with Information Flow

Mappl: A compiler that enables scalable inference by factorizing recursive probabilistic programs via continuation-passing-style (CPS) compilation and information-flow typing (with a denotational, logical-relations model).

Jianlin Li, Eric Wang, Yizhou Zhang

Acceptance rate: 27.64%, 89 accepted out of 322 submissions

[DOI | Artifact | TR | Talk | Poster version for Cheriton Symposium]

    POPL 2023
Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference

Fidelio: A compiler that embodies symbolic methods (e.g., a type system and program analysis) aiding neural-network–based inference.

Jianlin Li, Leni Ven, Pengyuan Shi, Yizhou Zhang

Acceptance rate: 27.31%, 74 accepted out of 271 submissions

[DOI | TR | Talk | Rehearsal]

Peer-Reviewed Publications (while at Saarland University)
    CAV 2021
Automated Safety Verification of Programs Invoking Neural Networks

Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmann, Yugesh Kothari, Jianlin Li, Jorge A. Navas, Valentin Wüstholz

Acceptance rate: 27.24%, 29 accepted out of 290 submissions

[DOI | PDF]

Peer-Reviewed Publications (while at ISCAS)
    TACAS 2021
Improving Neural Network Verification through Spurious Region Guided Refinement

Pengfei Yang, Renju eLi, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, and Lijun Zhang

Acceptance rate: 33.3%, 47 accepted out of 141 submissions

[DOI | PDF]

    ESEC/FSE 2020
PRODeep: A Platform for Robustness Verification of Deep Neural Networks

Renjue Li, Jianlin Li, Cheng-Chao Huang, Pengfei Yang, Xiaowei Huang, Lijun Zhang, Bai Xue, and Holger Hermanns

Acceptance rate: 28.06%, 101 accepted out of 360 submissions

[DOI | video]

    SAS 2019
Analyzing Deep Neural Networks With Symbolic Propagation: Towards Higher Precision and Faster Verification

Jianlin Li, Jiangchao Liu, Pengfei Yang, Liqian Chen, Xiaowei Huang, and Lijun Zhang

Acceptance rate: 40%, 20 accepted out of 50 submissions

[DOI | PDF]

    QEST 2018
Verifying Probabilistic Timed Automata Against ω-regular Dense-Time Properties

Hongfei Fu, Yi Li, and Jianlin Li

Acceptance rate: 47.06%, 24 accepted out of 51 submissions

[DOI | PDF]

Thesis
Design and Implementation of Probabilistic Programming Languages for Sound and Scalable Inference.

The compiler perspective leads to sound, scalable ways to automate probabilistic inference for a rich class of probabilistic models.

Compilers Venues Inference Methods Compilation Artifacts Keywords
Geni ICFP'25 Knowledge Compilation Probability Generating Functions Compiler Optimization
Mappl PLDI'24 Variable Elimination CPS-Transformed Factor Functions Program Partitioning
Fidelio POPL'23 Variational Inference Neural-Aided Guide Program Absolute Continuity

In a clever compiler for a probabilistic programming language, general-purpose compiler techniques can rival the power of domain-specific expertise and specialized decision procedures.

Jianlin Li, Ph.D. Thesis, University of Waterloo (in progress).

Symbolic Propagation Based Local Robustness Verification of Deep Neural Networks and Verification Platform

Jianlin Li. Master’s thesis. Institute of Software, Chinese Academy of Sciences, 2021.

Translating LTL to FDFA and FDFA Model Checking

Jianlin Li. Bachelor’s thesis. Nanjing University of Aeronautics and Astronautics, 2018.

Instructional Apprentice/Teaching Assistant

CS 450/650 Computer Architecture
CS 444/644 Compiler Construction
CS 245 & CS 245E  Logic and Computation
CS 241 Foundations of Sequential Programs

Other Activities
Sub-Reviewer: LICS 2018, TASE 2019, FM 2019, FMAC 2019, TACAS 2021, PLDI 2024, OOPSLA 2024.
Student Volunteer: CONCUR 2018, SSFM 2018 2019, LICS 2020.
Misc
I shoot cityscapes & architecture, landscapes, street photography, and portraits. I also enjoy karaoke and playing the guitar.