Welcome to Yichen Tao’s homepage!
I am a first-year Ph.D. student in Computer Science and Engineering at the University of Michigan, advised by Prof. Jean-Baptiste Jeannin in Michigan Aerospace and Robotics Verification Laboratory (MARVL) and Prof. Max New. Before that, I was an undergraduate student in Computer Science and Technology at Shanghai Jiao Tong University, working with Prof. Qinxiang Cao and Prof. Biaoshuai Tao.
Research Interests: Programming Languages, Formal Methods.
Software systems are pervasive in today’s society, and are becoming increasingly indispensable in people’s life. We can hardly live without software systems such as electronic payment, or aircraft flight control system, and our property and personal safety heavily relies on their correctness. However, it is getting tougher to build correct and bug-free programs due to the growing intricacy, and a minor fault may cause significant loss in crucial situations. Therefore, a remedy must be found to ameliorate this issue. From my perspective, the best tool to employ is Formal Verification and Programming Languages (PL) Theory. On the one hand, formally verified systems such as operating system kernels, file systems, and compilers, etc. have been shown to be more trustworthy and dependable compared with those whose correctness is established via other approaches such as testing and program analysis. On the other hand, PL theory enables rigorous program verification for practitioners and therefore improve the reliability of the programs.