Jianlin Herman Li

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 have a general interest in code-level verification of real-world software and interactive theorem proving, such as Coq, Agda, and Lean.

Currently, I am working with Yizhou on type system–based approaches for efficient, reliable, and certified probabilistic programming.

Peer-Reviewed Publications at University of Waterloo

ICFP 2025

Compiling with Generating Functions

Geni: A compiler uses generating functions to compactly and exactly represent probabilistic programs.

Jianlin Li, Oghenevwogaga Ebresafe, Yizhou Zhang

PLDI 2024

Compiling Probabilistic Programs for Variable Elimination with Information Flow

Mappl: A compiler factorizes recursive probabilistic programs for scalable inference.

Jianlin Li, Eric Wang, Yizhou Zhang

[ DOI | Artifact | TR ]

POPL 2023

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

Fidelio: Symbolic methods (a type system and an analysis) aid in neural-network-based inference.

Jianlin Li, Leni Ven, Pengyuan Shi, Yizhou Zhang

[DOI |TR]

Peer-Reviewed Publications 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

[DOI]

Peer-Reviewed Publications 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

[DOI]

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

[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

[DOI]

QEST 2018

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

Hongfei Fu, Yi Li, and Jianlin Li

[DOI]

Thesis

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.

Other Activities

Sub-Reviewer: LICS 2018, TASE 2019, FM 2019, FMAC 2019, TACAS 2021.
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.