New Homepage

https://jianlin-herman-li.github.io/

Old Homepage

I am a Ph.D student at PLG, University of Waterloo (started from Fall 2021). I am co-supervised by Ondřej Lhoták and Yizhou Zhang.

Research interests

I am generally interested in theorem proving and code-level verification of real-world software and theorem proving, such as certified system software, concurrent separation logic, and Coq.

Now I actively working with Yizhou on a type system approach of faithful guide generation for amortized probabilistic inference (mostly for compiled sequential importance sampling).

Education

• Master in Computer Science, University of Chinese Academy of Sciences, 2021
• Bachelor of Computer Science, Nanjing University of Aeronautics and Astronautics, 2018

Publications

1. Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference.
   Jianlin Li, Leni Ven, Pengyuan Shi, and Yizhou Zhang.
   POPL 2023 (to appear)
2. 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.
   CAV 2021 [paper]
3. 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.
   TACAS 2021
4. 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.
   ESEC/FSE 2020 [video]
5. 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.
   SAS 2019 [paper]
6. Verifying Probabilistic Timed Automata Against $\omega$-regular Dense-Time Properties.
   Hongfei Fu, Yi Li, and Jianlin Li.
   QEST 2018

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.

Talks

• Analyzing Deep Neural Networks With Symbolic Propagation: Towards Higher Precision and Faster Verification.
  In 26th Static Analysis Symposium, SAS 2019, Porto, Portugal, October, 2019,

Service

• Sub-Reviewer. LICS 2018. TASE 2019. FM 2019. FMAC 2019. TACAS 2021.
• Student Volunteer. CONCUR 2018, SSFM 2018, 2019. LICS 2020.

Course Projects

• Generalized Minsky machine halting $\preccurlyeq_m$ 2 counter machine halting in Coq.
• C(resp. Java)interprocedural points-to analysis in LLVM(resp. Soot).
• xv6 programming projects for OS.
• 5 stage pipelined MIPS-32 processor [Verilog Code].

Personal

I shoot landscapes, street photography, and portraits of friends in my spare time. [Gallery]