A separate compilation extension to standard ML. - David Swasey; Tom Murphy VII; Karl Crary; Robert Harper 001 (ML, 2006)

xDomain: cross-border proofs of access. - Lujo Bauer; Limin Jia 001; Michael K. Reiter; David Swasey (SACMAT, 2009)

Modeling and Enhancing Android's Permission System. - Elli Fragkaki; Lujo Bauer; Limin Jia 001; David Swasey (ESORICS, 2012)

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. - Ralf Jung 002; David Swasey; Filip Sieczkowski; Kasper Svendsen; Aaron Turon; Lars Birkedal; Derek Dreyer (POPL, 2015)

Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). - Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Marco Stronati; David Swasey (CoRR, 2017)

Robust and compositional verification of object capability patterns. - David Swasey; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2017)

Modular, Full-System Verification. - Gregory Malecha; Hoang-Hai Dang; Paolo G. Giarrusso; Simon Hudon; Jan-Oliver Kaiser; David Swasey (HotOS, 2025)