← Back

I am currently doing research with

Here are my research activities, most recent first:

Summer 2015 - Present

I am continuing to work with Anton Burtsev on the Lightweight Capability Domains project. We have a paper accepted to PLOS 2015.

Spring 2014 - Spring 2015

My work followed two fronts. First, I worked with Anton Burtsev on the Lightweight Capability Domains project and submitted a Bachelor's thesis on the work I did. My work included designing a simple KVM-style hypervisor for running kernel modules in isolation, and a small library kernel to support isolated code. The small library kernel was the most interesting part - I came up with a way to re-use the Linux slab allocator! We also presented a poster at OSDI 2014 in Denver:

Second, I worked with Ganesh and Alexey Solovyev on a new IEEE floating point formalization, to be used in the FPTaylor tool for automated error analysis of floating point programs. We presented at NSV 2015.

Fall 2013 - Spring 2014

In collaboration with the Verified Software Laboratory at the University of Delaware, I wrote a model for the semantics of CIVL-C, part of the CIVL framework, using PLT-Redex. Some of the project details can be found here.

Summer 2013

My summer consisted primarily of the following activities:

Through these efforts, we gained a better understanding of executable semantics tools, and how they can be used to describe the semantics of parallel programming languages (non-determinism, complicated state, etc.). We submitted a poster to the Supercomputing 2013 Conference:

I also did a small amount of work with KULFI, learned how to build custom compiler passes in LLVM, and experimented with other formal verification tools including UFO. As a side effect, I strengthened my skills in shell scripting, build tools, and virtual machines.