About me
Biography
I am a Ph.D student majoring in Computer Science at University of Colorado Boulder, co-advised by Bor-Yuh Evan Chang, Pavol Černý and Ashutosh Trivedi. I am a member of Programming Languages and Verification at the University of Colorado Boulder (CUPLV).
I received my master's degree from University of Colorado Boulder in 2017 (GPA: 3.92), and bachelor's degree from Nanjing University (Nanjing, China) in 2015.
I love writing code and I am very enthusiastic about developing tools that address real-world problems. My experience and expertise in Program Analysis and Verification brings me a unique and deep understanding of computer programming.
Research
My research interest is to develop and apply Program Analysis and Verification techniques for/into different real world problem domains.
My current research topic Resource and Cost Analysis of a program, which statically analyzes and verifies the upper bounds on resource and cost usage of a program, thus being fundamental to Cyber Security problems such as Denial-of-Service and Side Channel. I am also interested in adopting a type-system approach, because it is modular, fast and thus scalable to real-world programs.
Experience
I have been participating and funded by DARPA STAC program since 2015. I have attended six of the so-called "Engagement" events in STAC program, where our task is to either look for Denial-of-Service or Side Channel vulnerabilities in web applications, or prove their non-existence.
I have been designing and implementing scalable program analysis and verification tools mainly in Scala and Java. In my recently accepted paper, I implemented a tool in 5k lines of Scala code, using The Checker Framework and Microsoft Z3 Theorem Prover. My tool analyzed and verified 12 benchmark programs with over 180k lines of Java code. The Checker Framework extends the original Java type system with more powerful and useful annotations, enabling software developers to detect and prevent errors more effectively in Java programs.
Publications
- Lu, Tianhan, Pavol Černý, Bor-Yuh Evan Chang, and Ashutosh Trivedi. "Type-directed bounding of collections in reactive programs." In International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 275-296. Springer, Cham, 2019. [PDF]