Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language. - Jay Bosamiya; Sydney Gibson; Yao Li 004; Bryan Parno; Chris Hawblitzel (VSTTE, 2020)

Steel: proof-oriented programming in a dependently typed concurrent separation logic. - Aymeric Fromherz; Aseem Rastogi; Nikhil Swamy; Sydney Gibson; Guido Martínez; Denis Merigoux; Tahina Ramananandro (Proc. ACM Program. Lang., 2021)

Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares. - Yi Zhou 025; Sydney Gibson; Sarah Cai; Menucha Winchell; Bryan Parno (CCS, 2023)

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System. - Joshua Gancher; Sydney Gibson; Pratap Singh; Samvid Dharanikota; Bryan Parno (SP, 2023)