In addition to this curriculum vitae, I also provide a simplified résumé.


Johns Hopkins University August 2015
Ph.D., Computer Science

Confidence in Confinement: An Axiom-free, Mechanized Verification of Confinement in Capability-based Systems [PDF] [LaTeX] [Source]

Advisor: Dr. Jonathan S. Shapiro

Gustavus Adolphus College May 2002

B.A., Computer Science

Technical Expertise

Professional: Java, JDB, Perl, Python, SQL, C, C++, GDB, GNU Make, Bash, LotusScript, Lotus @Commands, HTML, CSS, JavaScript, Linux kernel tracing, Linux VFS, Linux kernel modules, ACL2, Isabelle/HOL, TWELF, Coq, OCaml, SML, LaTeX, Git, Mercurial, SVN, CVS, QEMU.

Personal: Haskell, Agda, Jekyll, Liquid, Sass, Arduino, Raspberry Pi, OpenSCAD.


Johns Hopkins University 2003-2015

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.

Johns Hopkins University 2009

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.

Johns Hopkins University 2006-2009

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.

Johns Hopkins University 2007

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.

Johns Hopkins University 2003-2006

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.

Oracular Systems and Software 2002-2003

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.

Virtual Information Systems 2000-2001

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.

Gustavus Adolphus College 2000-2002

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.


M. S. Doerrie, Confidence in Confinement: An Axiom-free, Mechanized Verification of Confinement in Capability-based Systems , Ph. D. Dissertation, Johns Hopkins University, July 2015. [LaTeX] [Source]

J. S. Shapiro, S. Sridhar, S. Doerrie, M. Miller, E. Northup. BitC Language Specification, June 2006.

J. S. Shapiro, M. S. Doerrie, E. Northup, S. Sridhar, and M. Miller, Towards a Verified, General-Purpose Operating System Kernel, Proc. 2004 NICTA Operating Systems Verification Workshop, 2004.

Honors and Awards

1998 - 2001 Gustavus Dean’s List

1998 - 2001 Trustee Scholarship

1998 - 2001 Norelius Service Award

1998 BSA Eagle Scout