I am currently doing research with
- Anton Burtsev and the Flux Group, since April 2014
- Ganesh Gopalakrishnan and the Gauss Group, since Summer 2013
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.
My summer consisted primarily of the following activities:
- Self-study of operational semantics and term re-writing
- Learning how to use the K Framework and PLT-Redex, executable semantics tools
- Learning MPI
- Learning ISP and DAMPI, tools developed by the Gauss Group for model checking MPI programs
- Describing the semantics of MPI and ISP using the K Framework
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.