Vita

B.A., Computer Science

Graduate Researcher, Systems Research Laboratory

Core Technologies: Coq, ACL2, TWELF, Isabelle/HOL, OCaml, SML, Perl, GNU Make, Latex, Mercurial, GIT.

• Conclusively demonstrated that capability-based systems can enforce confinement by leveraging mechanical verification using the Coq proof assistant.
• Increased confidence in the model and widened its future applicability by providing permission propagation theorems independent of any specific policy that are subsequently applied to the confinement problem.
• Hardened the model by providing a general implementation that can be refined to describe any capability system and completes the model for an axiom-free proof.
• Critically assessed multiple first-order and higher-order proof systems including ACL2, TWELF, Isabelle/HOL, and Coq.
• Ensured the Coyotos and BitC projects would be fit for future verification by providing continual feedback through their development.

Teaching Assistant to Dr. Jonathan S. Shapiro, Microkernels

Core Technologies: C, C++, GNU Make, QEMU, GDB, GIT, Mercurial.

• Provided a constructive environment by assisting students with development and debugging in the Coyotos microkernel.
• Responded to student needs by offering lengthy mentoring sessions every night.

Instructor, Operating Systems

Core Technologies: C, GNU Make, QEMU, GDB, GIT, Mercurial, Linux kernel modules, Linux VFS.

• Responsible for all aspects of course execution.
• Provided an extremely practical, hands-on, and critical examination of operating system design reflecting both academic and practical perspectives.
• Improved the scope of the course by designing and presenting novel materials on 64-bit memory architectures, Linux kernel module development and in-kernel debugging, and capability-based systems.
• Prepared students professionally with advanced course material including the slab allocator, file-system implementations and Linux VFS, microkernels, and virtualization techniques.

Lecturer, “TWELF Lecture series,” Systems Research Laboratory

Core Technologies: TWELF.

• Introduced the Systems Research Laboratory to verification techniques in TWELF by designing and presenting a half-semester lecture series.
• Communicated topics in advanced type theory and totality analysis and their relationship to mathematical proofs.

Research Assistant, Systems Research Laboratory

Core Technologies: C, GNU Make, GDB, GIT, Mercurial, Linux kernel tracing, Linux VFS.

• Was a key participant in the coevolution of BitC and Coyotos.
• Reconciled the Intel paging mechanism with Coyotos’ general-purpose guarded page tables.
• Motivated guarded page tables by simulating process behavior taken from traces in Linux and demonstrating that guarded page tables would not add substantial overhead.
• Guided early BitC language development through issues regarding formalization and verification.

Software Consultant and System Administrator

Core Technologies: Java, HTML, JavaScript, CSS, LotusScript, Lotus @Commands, SQL, SVN.

• Improved corporate utility to clients by producing rapid prototypes of software services.
• Adapted to client software configurations when realizing prototypes into high-quality deliverables.
• Increased system uptime for clients and the company by diagnosing server and service issues.

Developer Internship

Core Technologies: LotusScript, Lotus @Commands, HTML, JavaScript, CSS, CVS.

• Improved metrics in reported billable hours by updating the internal billing service.
• Increased client efficiency by developing digital-workflow applications for existing business practices.

Electronic Reserves Developer

Core Technologies: Perl, SQL, GNU Make, HTML, JavaScript.

• Worked within a self-directed and self-managed team to design and deploy the Gustavus Library Electronic Reserves system.
• Took personal responsibility for the system backend and data processing.