William Mansky

Publication Activity (10 Years)

Years Active: 2010-2024
Publications (10 Years): 17

Top Topics

Concurrent Programs

Logical Representation

Top Venues

Proc. ACM Program. Lang.

Publications

Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang
Compositional Verification of Concurrent C Programs with Search Structure Templates. CPP (2024)
William Mansky, Ke Du
An Iris Instance for Verifying CompCert C Programs. Proc. ACM Program. Lang. 8 (POPL) (2024)
Roshan Sharma, Shengyi Wang, Alexander Oey, Anastasiia Evdokimova, Lennart Beringer, William Mansky
Proving Logical Atomicity using Lock Invariants. CoRR (2023)
Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer
Compass: strong and compositional library specifications in relaxed memory separation logic. PLDI (2022)
William Mansky
Bringing Iris into the Verified Software Toolchain. CoRR (2022)
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic
Verifying an HTTP Key-Value Server with Interaction Trees and VST. ITP (2021)
William Mansky, Wolf Honoré, Andrew W. Appel
Connecting Higher-Order Separation Logic to a First-Order Outside World. ESOP (2020)
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
From C to interaction trees: specifying, verifying, and testing a networked server. CPP (2019)
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. CoRR (2018)
Yuanfeng Peng, Christian DeLozier, Ariel Eizenberg, William Mansky, Joseph Devietti
SLIMFAST: Reducing Metadata Redundancy in Sound and Complete Dynamic Data Race Detection. IPDPS (2018)
Dmitri Garbuzov, William Mansky, Christine Rizkallah, Steve Zdancewic
Structural Operational Semantics for Control Flow Graph Machines. CoRR (2018)
Ariel Eizenberg, Yuanfeng Peng, Toma Pigli, William Mansky, Joseph Devietti
BARRACUDA: binary-level analysis of runtime RAces in CUDA programs. PLDI (2017)
William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti
Verifying dynamic race detection. CPP (2017)
William Mansky, Andrew W. Appel, Aleksey Nogin
A verified messaging system. Proc. ACM Program. Lang. 1 (OOPSLA) (2017)
William Mansky, Elsa L. Gunter, Dennis Griffith, Michael D. Adams
Specifying and executing optimizations for generalized control flow graphs. Sci. Comput. Program. 130 (2016)
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
A formal C memory model supporting integer-pointer casts. PLDI (2015)
William Mansky, Dmitri Garbuzov, Steve Zdancewic
An Axiomatic Specification for Sequential Memory Models. CAV (2) (2015)
Liyi Li, Elsa L. Gunter, William Mansky
Symbolic Analysis Tools for CSP. ICTAC (2014)
William Mansky, Elsa L. Gunter
Verifying Optimizations for Concurrent Programs. WPTE@RTA/TLCA (2014)
William Mansky, Dennis Griffith, Elsa L. Gunter
Specifying and Executing Optimizations for Parallel Programs. GRAPHITE (2014)
William Mansky, Elsa L. Gunter
Using Locales to Define a Rely-Guarantee Temporal Logic. ITP (2012)
Ellen J. Bass, Matthew L. Bolton, Karen M. Feigh, Dennis Griffith, Elsa L. Gunter, William Mansky, John M. Rushby
Toward a multi-method approach to formalizing human-automation interaction and human-human communications. SMC (2011)
William Mansky, Elsa L. Gunter
A Framework for Formal Verification of Compiler Optimizations. ITP (2010)