Lefan Zhang


About me

I’m a 4th year PhD student in Department of Computer Science, University of Chicago, advised by Prof. Shan Lu.

I’m currently working on applying formal methods to provide better end-user programming experience in smart home. More specifically, I’m interested in developing tools that could help users to debug, diagnose or synthesize trigger-action programs in their smart home.

I got my bachelor degree in electronic engineering from Tsinghua University in 2017.

Research Project


It is a tool that uses formal specifications to verify, debug or synthesize trigger-action programs in smart home. It provides a user-friendly interface allowing users to turn their requirements into formal specifications from only clicking. By analyzing automata of the current system, it identifies potential violations and suggests patches.

A demo could be found here (please watch with subtitles on).


It is a debugger and synthesizer for trigger-action programs. It learns TAP patches from users' traces in their smart homes. It symbolizes trigger-action programming space, re-executes users' traces and finds TAP patches that can potentially automate users' manual behaviors.

A lightning presentation can be found here.




Email: lefanz at uchicago dot edu

Address: 5730 S Ellis Ave, Chicago, IL 60637


My resume can be found here.