Online Z3 Guide (2022.6 - 2022.9)

I implemented the Online Z3 Guide, a 100% client-side web-based programming/learning environment for Z3 during my Research Internship this summer (2022) at Microsoft Research, working with Ayana Monroe, Dr. Nikolaj Bjorner and Dr. Peli de Halleux. The development of Z3Guide adopted an iterative design, and has been well perceived by teachers and learners of Z3. It is also a first step towards reviving rise4fun, a legacy web environment for research tools developed at RiSE @ MSR. See my fork of the version concluded at the end of my internship, or here for the most recent official Z3Guide.

Live Synthesis Recognition (2022.6 - Present)

Live Programming + Copilot …? Stay tuned!

Step’n’Tune (2021.12 - Present)

The fulfillment of live programming results in program outputs that are always up-to-date with the code. In non-terminating systems, such fulfillment could fail when specific contexts are not provided. To address this problem, we proposed a new paradigm called live programming with output interactions, which obtains contexts for live programming through user interactions with the program output and provides live feedback on the output given such contexts. We implemented this paradigm in a system for developing GUI applications called Step’n’Tune. Step’n’Tune allows the user to alternate between coding and interacting with the UI in the same interface, live-visualizes all the execution traces and intermediate UI changes per interaction, and keeps the execution and UI traces up-to-date with the code.

SnipPy+ (2021.3 - 2021.9)

Built on top of SnipPy, SnipPy+ features a new interaction flow where the user can constantly interact with the synthesizer without leaving and restarting the specifications writing process: they can (1) see synthesis results as they are typing in specifications and (2) keep modifying the specifications / inspecting new synthesis results, until they intend to exit the process.

PopPy (2021.1 - 2021.3) [paper]

I explored the idea of PopPy in collaboration with Kasra Ferdowsi in a class project. Also built on top of SnipPy, PopPy allows the user to write partial instead of full specifications for program synthesis, which can be especially useful when the specs involve long, complicated data structures.

Projection Boxes for Education (PB4Edu) (2020.8 - 2021.3) [paper] [talk]

We used Projection Boxes, a Live Programming visualization, in an introductory programming class with 600+ students at UCSD over one academic quarter, and found that students preferred Projection Boxes to the baseline IDE and considered them helpful for their learning.

Venbrace (2019.1 - 2020.7) [thesis] [poster] [demo]

Venbrace is a textual representation for the block-based MIT App Inventor. Its design is principled and empirically evaluated through two user studies. Although no conclusive evidence was found from either study, this project is my first exploration in the space of human-centric programming language design.

Visualizing TwitterTrails Stories (2018.1 - 2018.10) [poster]

TwitterTrails is a tool that allows members of the media to track the trustworthiness of stories shared on Twitter co-built by Panagiotis Metaxas at Wellesley College. My prototype visualizes the stories (circles) and their tags (linked lines connecting the circles to the dots on the outer bigger circle) alongside their magnitudes of spread (sizes of circles) and levels of trustworthiness (blue=undisputed, red=doubtful) as determined by TwitterTrails’ algorithm. With this interactive visualization, users are able to focus on stories/tags of their interest through the filtering mechanism and interpret metrics of a story more easily without examining its associated tweets.