Liyi Li
Position
- Assistant Professor
I am an assistant professor in the CS department. I earned my PhD at the University of Illinois under the supervision of Elsa Gunter, with the topic of compiler verification, which connects the fields of compilers, programming languages, and formal methods. Mainly, we intend to develop trustworthy software using the compiler field. The experience fixes my “research personality”, in the sense that my main research focus is to “compile” a hard problem to a solution to a similar problem in another field. After graduation, I had a postdoc experience at the University of Maryland, where I practiced my research personality to work in quantum computing. Mainly, I utilized compiler and verification techniques to optimize, analyze, and verify quantum programs. Another branch of my work is to continue my work with compiler verification by developing memory-safe compilers, such as the Checked-C work, a memory-safe dialect of C. After I joined Iowa State University, I expanded my domain knowledge to border software engineering techniques. I tried to utilize different software engineering tools, such as genetic algorithms and probabilistic model-checking techniques, to help analyze program properties and improve program performance.
Research Interests: Formal methods; programming languages; software engineering; quantum computing; mathematical semantics of programming languages; formal reasoning about human-computer systems; formal reasoning about security; proof theory and type theory; programming languages for quantum computing; formal and practical verification tools for languages including quantum language; methodology transformation for building trustworthy software development
Research Interests: Formal methods; programming languages; software engineering; quantum computing; mathematical semantics of programming languages; formal reasoning about human-computer systems; formal reasoning about security; proof theory and type theory; programming languages for quantum computing; formal and practical verification tools for languages including quantum language; methodology transformation for building trustworthy software development
Contact
Email
liyili2@iastate.edu
Phone
(515)294-0303
Contact Info
205 Atanasoff Hall
2434 Osborn Dr
Ames
,
Iowa
50011
Education
- B.S., Computer Science, University of Illinois at Urbana-Champaign
- M.S., Computer Science, University of Illinois at Urbana-Champaign
- Ph.D., Computer Science, University of Illinois at Urbana-Champaign
Publications
- Conference
- Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu, Qafny: A Quantum-Program Verifier, ECOOP 2024
- Finn Voichick, Liyi Li, Robert Rand, Michael Hicks, Qunity: A Unified Language for Quantum and Classical Computing, POPL 2023
- Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, Michael Hicks, Verified Compilation of Quantum Oracles, OOPSLA 2022
- Liyi Li, Yiyun Liu, Deena Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks, A Formal Model of Checked C, CSF 2022
- Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks, Proving Quantum Programs Correct, ITP 2021
- Liyi Li and Elsa L. Gunter, A Complete Semantics of K and Its Translation to Isabelle, ICTAC 2021
- Kesha Hietala, Liyi Li, Akshaj Gaur, Aaron Green, Robert Rand, Xiaodi Wu, Michael Hicks, Expanding the VOQC Toolkit, PLanQC 2021
- Liyi Li and Elsa L. Gunter, K-LLVM: A Relatively Complete Semantics of LLVM IR, ECOOP 2020
- Liyi Li and Elsa L. Gunter, Per-Location Simulation, NFM 2020
- Liyi Li and Elsa L. Gunter, IsaK-Static: A Complete Static Semantics of K, FACS 2018
- Liyi Li and Elsa L. Gunter, A method to translate order-sorted algebras to many-sorted algebras, WPTE 2017
- Liyi Li, Elsa L. Gunter, William Mansky. Symbolic Analysis Tools for CSP, ICTAC 2014
- Journal
- Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, Xiaodi Wu, A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm, PNAS journal, 2023
- Kesha Hietala, Robert Rand, Liyi Li, Shih-Han Hung, Xiaodi Wu, Michael Hicks, A Verified Optimizer for Quantum Circuits, TOPLAS journal, 2023
- Liyi Li, Yiyun Liu, Deena Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks, A Formal Model of Checked C, Journal of Computer Security 2023
Research Funding
- CCF2422127: Collaborative Research: FMitF: Track I: JIVe: Just in Time Verification for High Performance Compilers, 09/24-08/27, $1M, PI
External Reviewing
- Program Committees
- SPIN 2022: 28th International Symposium on Model Checking of Software
- OOPSLA 2024
- Extended Review and Artifact Evaluation Committee
- OOPSLA 2023
- Reviewer
- PLDI 2023
- PeerJ Computer Science
Awards
- 2020 UMD Victor Basili Postdoc
- 2019 UIUC Spring Outstanding Teaching Assistant Award
- UIUC University Honor 2012 (Bronze Tablet)
Advised Collaborators
- Mingwei Zhu (University of Maryland)
- Alexander Nicolellis (Iowa State University)
- Son Vu (Iowa State University)
- Jae Swanepoel (Iowa State University)
Current Students
- Le Chang (University of Maryland)
- Jason Liao (University of Maryland)
- Chandeepa Dissanayake (Iowa State University)
- Saitej Yavvari (Iowa State University)
- Pavani Ronanki (Iowa State University)
- Arjun Patel (Iowa State University)
- Junhyung Shim (Iowa State University)
- Logan Brown (Iowa State University)
- Henry Allard (Iowa State University)
- Miles Borgstadt (Iowa State University)
Anshu Sharma (William and Mary)