William Mansky

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