Tianchuan Lin (林田川)

I am a third-year undergraduate student of Computer Science at ACM Class, Shanghai Jiao Tong University.

I am interested in Formal Verification, Programming Languages and Distributed Systems. I achieved A+ in the following courses: Programming Verification, Mathematical Logic, Compiler Design and Implementation, Distributed Systems.

• Email: [email protected]
• Github: 1024th

Research Interests

I am interested in building reliable and efficient software systems.

Formal methods are a powerful tool for building reliable software. They can be used to prove that software is correct. However, formal methods are not widely used because they require a lot of human effort and expertise. How to make formal methods more accessible and practical attracts me.

I am also interested in optimizing the performance of software systems, especially for Machine Learning and Distributed Systems. I am fascinated by the practical ideas and techniques that can be used to improve the performance of software systems.

Projects

• Correctness Verification of the Use/Def Analysis: Course project of CS 2206, Programming Verification.
  We use Coq to define and prove the correctness of the Use/Def analysis of a simple programming language. We also prove the equivalence of two different iterative algorithms for the analysis.
• Google File System (Github): Course project of Distributed Systems, 2023 Summer.
  Google File System is a distributed file system developed by Google. This project is a simplified implementation of GFS, written in Go.
• Mx-Compiler (Github): Course Project of Compiler Design and Implementation.
  A compiler for Mx* language, a subset of C/Java. The compiler is written in Java and generates RISC-V assembly code. LLVM IR is used as the intermediate representation.
  Some optimizations are implemented, including Aggressive Dead Code Elimination, Loop Invariant Code Motion, etc.
• Distributed Hash Table (GitHub): Course project of PPCA 2022 DHT.
  Two protocols are implemented: Chord and Kademlia. An application layer is built on top of the protocols to provide file sharing service similar to BitTorrent. The project is written in Go.
• Fine-tuning Transformer Model for Trickier Symbolic Integration: Course project of Machine Learning.
  Based on Facebook AI's ‘Deep Learning for Symbolic Mathematics’, we fine-tune the model to solve trickier symbolic integrals.
• RV32I CPU (Github): Course project of Computer Architecture.
  A Tomasulo-based out-of-order CPU with Instruction Cache and Branch Prediction. The CPU is written in Verilog and executed on FPGA.

Experience

• Mathematical Logic (Fall 2023), Teaching Assistant. The syllabus is similar to previous year.
• Programming Practice 2023, Teaching Assistant. I improved the course project Distribute Hash Table.
• Programming (C++) 2022, Teaching Assistant. I improved the course project.
• CCF Certified Software Professional - Senior (CSP-S) 2019, the first prize in province.
  CSP-S is equivalent to National Olympiad in Informatics in Provinces (NOIP). CCF is the abbreviation of China Computer Federation.

Skills

• Programming Languages: C/C++, Java, Python, Go, Verilog, Coq, Dafny.
• Tools: Git, Linux, Vim, SSH, LaTeX.