Higher-Order Separation Logic in Isabelle/HOLCF. - Carsten Varming; Lars Birkedal (MFPS, 2008)

Some Domain Theory and Denotational Semantics in Coq. - Nick Benton; Andrew Kennedy; Carsten Varming (TPHOLs, 2009)

Semantic-based Automated Reasoning for AWS Access Policies using SMT. - John Backes; Pauline Bolignano; Byron Cook; Catherine Dodge; Andrew Gacek; Kasper Søe Luckow; Neha Rungta; Oksana Tkachuk; Carsten Varming (FMCAD, 2018)

Reachability Analysis for AWS-Based Networks. - John Backes; Sam Bayless; Byron Cook; Catherine Dodge; Andrew Gacek; Alan J. Hu; Temesghen Kahsai; Bill Kocik; Evgenii Kotelnikov; Jure Kukovec; Sean McLaughlin; Jason Reed 004; et al. (CAV (2), 2019)

One-Click Formal Methods. - John Backes; Pauline Bolignano; Byron Cook; Andrew Gacek; Kasper Søe Luckow; Neha Rungta; Martin Schäf; Cole Schlesinger; Rima Tanash; Carsten Varming; Michael W. Whalen (IEEE Softw., 2019)

Stratified Abstraction of Access Control Policies. - John Backes; Ulises Berrueco; Tyler Bray; Daniel Brim; Byron Cook; Andrew Gacek; Ranjit Jhala; Kasper Søe Luckow; Sean McLaughlin; Madhav Menon; Daniel Peebles; Ujjwal Pugalia; et al. (CAV (1), 2020)

Block public access: trust safety verification of access control policies. - Malik Bouchet; Byron Cook; Bryant Cutler; Anna Druzkina; Andrew Gacek; Liana Hadarean; Ranjit Jhala; Brad Marshall; Daniel Peebles; Neha Rungta; Cole Schlesinger; Chriss Stephens; et al. (ESEC/SIGSOFT FSE, 2020)