Tianfan Xu

Home Institution
The University of Illinois at Urbana-Champaign

Year Participated
2022

Year in School
Undergraduate

REU Faculty Mentor
Charith Mendis

Research Area Interest
Programming Languages, Formal Methods, and Software Engineering

Project Title
Developing operation semantics for XLA tensor operations in Rosette

Biography & Research Abstract

Abstract:

This research project aims to design a rewrite system of the semantic operations of XLA architecture and formally prove tensor rewrite rules based on these. In particular, I have gone through the idea of operational semantics, learned and used the Rosette language for symbolic verifications, and modeled the DotGeneral operation in the XLA HLO so far. I would also produce a few tensor rewrite rules.

Bio:

My name is Tianfan Xu, and I am a Junior student at UIUC majoring in Math and CS. This summer, I will be working with Professor Mendis on the verification of tensor programs. In addition to program verification, I am also interested in the area of scientific computing, and I am fascinated by the idea of converting analytically “unsolvable” problems to computable things in reality.

I am looking forward to getting hands-on experience and producing meaningful results during this REU program.