A Framework for Formal Verification of Compiler Optimizations. - William Mansky; Elsa L. Gunter (ITP, 2010)

Toward a multi-method approach to formalizing human-automation interaction and human-human communications. - Ellen J. Bass; Matthew L. Bolton; Karen M. Feigh; Dennis Griffith; Elsa L. Gunter; William Mansky; John M. Rushby (SMC, 2011)

Using Locales to Define a Rely-Guarantee Temporal Logic. - William Mansky; Elsa L. Gunter (ITP, 2012)

Symbolic Analysis Tools for CSP. - Liyi Li 002; Elsa L. Gunter; William Mansky (ICTAC, 2014)

Verifying Optimizations for Concurrent Programs. - William Mansky; Elsa L. Gunter (WPTE@RTA/TLCA, 2014)

Specifying and Executing Optimizations for Parallel Programs. - William Mansky; Dennis Griffith; Elsa L. Gunter (GRAPHITE, 2014)

Specifying and verifying program transformations with PTRANS - William Mansky (2014)

An Axiomatic Specification for Sequential Memory Models. - William Mansky; Dmitri Garbuzov; Steve Zdancewic (CAV (2), 2015)

A formal C memory model supporting integer-pointer casts. - Jeehoon Kang; Chung-Kil Hur; William Mansky; Dmitri Garbuzov; Steve Zdancewic; Viktor Vafeiadis (PLDI, 2015)

Specifying and executing optimizations for generalized control flow graphs. - William Mansky; Elsa L. Gunter; Dennis Griffith; Michael D. Adams 001 (Sci. Comput. Program., 2016)

Verifying dynamic race detection. - William Mansky; Yuanfeng Peng; Steve Zdancewic; Joseph Devietti (CPP, 2017)

BARRACUDA: binary-level analysis of runtime RAces in CUDA programs. - Ariel Eizenberg; Yuanfeng Peng; Toma Pigli; William Mansky; Joseph Devietti (PLDI, 2017)

A verified messaging system. - William Mansky; Andrew W. Appel; Aleksey Nogin (Proc. ACM Program. Lang., 2017)

SLIMFAST: Reducing Metadata Redundancy in Sound and Complete Dynamic Data Race Detection. - Yuanfeng Peng; Christian DeLozier; Ariel Eizenberg; William Mansky; Joseph Devietti (IPDPS, 2018)

Structural Operational Semantics for Control Flow Graph Machines. - Dmitri Garbuzov; William Mansky; Christine Rizkallah; Steve Zdancewic (CoRR, 2018)

From C to interaction trees: specifying, verifying, and testing a networked server. - Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; Wolf Honoré; William Mansky; Benjamin C. Pierce; Steve Zdancewic (CPP, 2019)

Connecting Higher-Order Separation Logic to a First-Order Outside World. - William Mansky; Wolf Honoré; Andrew W. Appel (ESOP, 2020)

Verifying an HTTP Key-Value Server with Interaction Trees and VST. - Hengchu Zhang; Wolf Honoré; Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; William Mansky; Benjamin C. Pierce; Steve Zdancewic (ITP, 2021)

Compass: strong and compositional library specifications in relaxed memory separation logic. - Hoang-Hai Dang; Jaehwang Jung; Jaemin Choi; Duc-Than Nguyen; William Mansky; Jeehoon Kang; Derek Dreyer (PLDI, 2022)

Bringing Iris into the Verified Software Toolchain. - William Mansky (CoRR, 2022)

Proving Logical Atomicity using Lock Invariants. - Roshan Sharma; Shengyi Wang; Alexander Oey; Anastasiia Evdokimova; Lennart Beringer; William Mansky (CoRR, 2023)

Compositional Verification of Concurrent C Programs with Search Structure Templates. - Duc-Than Nguyen; Lennart Beringer; William Mansky; Shengyi Wang (CPP, 2024)

An Iris Instance for Verifying CompCert C Programs. - William Mansky; Ke Du 002 (Proc. ACM Program. Lang., 2024)