Research

Current Projects

• FlowBook: aJupyterLab extension that enforces rerun consistency: re-executing any cell from the current state would produce a result consistent with a top-to-bottom execution of the notebook, regardless of which cells have been run, modified, and rerun.

• Flowco: a system for authoring data analysis workflows with LLM assistance at every stage of the process. Flowco employs a dataflow programming model that serves as a foundation for reliable LLM-centric programming.

• Chat: an AI-based debugging assistant for C/C++/Python/Rust code that integrates large language models into a standard debugger to help debug your code.

• Pythoness: automatically generate Python code from natural language descriptions and tests.

• Melvin: verifies the functional correctness of concurrent programs modularly using Mover Logic.

• Keystone: specifying and reasoning about thread interference via mover logic.

Software and Research Artifacts

• Anchor Verifier Artifact
• VerifiedFT Artifact
• BigFoot Artifact
• RoadRunner Dynamic Analysis Framework

Various Tutorial, Workshop, and Conference Materials

• PLDI 2021 (General Chair)
• UPMARC 2014 Summer School lectures on Analysis Techniques to Detect Concurrency Errors
• RV 2012 Tutorial on Dynamic Analyses for Data-Race Detection
• PASTE ’13 (PC Cochair)
• Summer School on Software Reliability Lectures