David Swasey
Ph.D. student
MPI-SWS & Saarland University

I am a Ph.D. student studying Computer Science at the Max Planck Institute for Software Systems (MPI-SWS), co-advised by Derek Dreyer and Deepak Garg. Prior to joining the MPI-SWS in 2012, I worked as a research programmer at Carnegie Mellon University under the direction of Lujo Bauer (2006–12), Bob Harper (1998–2006), and Roger Dannenberg (1994–98). Please see my CV for the full story.

Research Interests

• Programming language design and implementation, type systems, and type theory.
• Logical frameworks, proof assistants, automated deduction, and verification.
• Computer security and privacy.

I am interested in Kripke models and logics for message-passing concurrency; for example, in the design of concurrency logics that support compositional verification of security protocols.

Publications

• Robust and Compositional Verification of Object Capability Patterns.
  David Swasey, Deepak Garg, and Derek Dreyer.
  Conditionally accepted to appear in OOPSLA 2017.
  • manuscript (abstract.txt), Coq development, VM image (an OVF archive with CoqIDE and a pre-compiled Coq development)
• Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning.
  Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer.
  In POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 637–650, Mumbai, India, January 2015.
  • article (abstract.txt), publisher's site
  • Web site with technical appendix and Coq source
• Modeling and enhancing Android's permission system.
  Elli Fragkaki, Lujo Bauer, Limin Jia, and David Swasey.
  In Computer Security — ESORICS 2012 — 17th European Symposium on Research in Computer Security, pages 1–18, Pisa, Italy, September 2012. Springer LNCS 7459.
  • article (abstract.txt), publisher's site
  • technical report: Carnegie Mellon University CyLab Technical Report CMU-CyLab-11-020, April 2012.
• xDomain: Cross-border proofs of access.
  Lujo Bauer, Limin Jia, Michael K. Reiter, and David Swasey.
  In SACMAT '09: Proceedings of the 14th ACM Symposium on Access Control Models and Technologies, pages 43–52, Stresa, Italy, June 2009.
  • article (abstract.txt), publisher's site
  • technical report: Carnegie Mellon University CyLab Technical Report CMU-CyLab-09-005, March 2009.
• A separate compilation extension to Standard ML.
  David Swasey, Tom Murphy VII, Karl Crary, and Robert Harper.
  In ML '06: Proceedings of the 2006 ACM SIGPLAN Workshop on ML, pages 32–42, Portland, Oregon, USA, September 2006.
  • article (abstract.txt), publisher's site
  • technical report: Carnegie Mellon University School of Computer Science Technical Report CMU-CS-06-104R, September 2006.
    This is a significantly expanded version of our ML '06 paper.
  • preliminary TR (abstract.txt): Carnegie Mellon University School of Computer Science Technical Report CMU-CS-06-104, January 2006.
    Superseded by our ML '06 paper.