My research group builds a variety of software systems in the course of our research. These are the systems that we are actively building:
SMT-Based Robot Transition Repair (SRTR): The SRTR project is a suite of programming tools for the working roboticist. Robot control programs suffer failures that are exceptionally hard to fix: some failures are unobservable (by the robot), others occur due to environmental factors, and recovery sometimes requires human intervention. SRTR provides a DSL for writing robot control programs, and a semi-automated program synthesis and repair tools. Portions of SRTR are described in research papers (IJCAI 2018 and CoRL 2020).
Containerless: A serverless computing platform that transparently uses language-based techniques to isolate and accelerate serverless functions when possible, and falls back to virtualization only when necessary.
A lot of my current work is focused on building better abstractions for WebAssembly. Our primary project in this space is not yet released, but we have written up some of our work on WebAssembly benchmarking (ATC 2019) and continuations for WebAssembly (DLS 2020).
Here are some past projects that are no longer in active development, in chronological order:
PANE: An SDN controller that allows safe, decentralized network configuration. PANE policies are written in a domain-specific language, and it has a compiler and runtime system that realizes the policies in OpenFlow. PANE was the foundation for Andrew Ferguson’s dissertation and is also described in a series of research papers (HotICE 2012], HotSDN 2012, and SIGCOMM 2013).
Frenetic: A language for programming software-defined networks. PANE borrowed many ideas from Frenetic, and I joined the Frenetic project two years after its inception. During my postdoc, I led the development of a new compiler and runtime system for Frenetic, and helped evolve its language (NetKAT). My work on Frenetic is described in a series of research papers (PLDI 2013, POPL 2014, and ICFP 2015).
Rehearsal: A verification tool for Puppet, which is an industrial DSL for writing system configurations. We used Rehearsal to build Tortoise, which is an automated configuration repair tool. Both are described in research papers (PLDI 2016 and ASE 2017).