The University of Illinois at Urbana-Champaign
Year in School
REU Faculty Mentor
Research Area Interest
Programming Languages, Formal Methods, and Software Engineering
Developing operation semantics for XLA tensor operations in Rosette
Biography & Research 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.
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.