Introduction
- 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. POPL 2024.
- Bringing Iris into the Verified Software Toolchain, William Mansky. arXiv, 2022.
- Proving Logical Atomicity using Lock Invariants, Roshan Sharma, Shengyi Wang, Alexander Oey, Anastasiia Evdokimova, Lennart Beringer, William Mansky. Presented at ASL 2022.
- 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.
- Verifying an HTTP Key-Value Server with Interaction Trees and VST, Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, Steve Zdancewic. ITP 2021.
- Connecting Higher-Order Separation Logic to a First-Order Outside World, William Mansky, Wolf Honore, Andrew W. Appel. ESOP 2020.
- From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honore, William Mansky, Benjamin C. Pierce, Steve Zdancewic. CPP 2019.
- A Verified Messaging System, William Mansky, Andrew W. Appel, Aleksey Nogin. OOPSLA 2017.
- BARRACUDA: Binary-level Analysis of Runtime RAces in CUDA Programs, Ariel Eizenberg, Yuanfeng Peng, Toma Pigli, William Mansky, Joseph Devietti. PLDI 2017.
- Verifying Dynamic Race Detection, William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti. CPP 2017.
- Specifying and Executing Optimizations for Generalized Control Flow Graphs, William Mansky, Elsa L. Gunter, Dennis Griffith, Michael D. Adams. Science of Computer Programming vol. 130, 2016.
- An Axiomatic Specification for Sequential Memory Models, William Mansky, Dmitri Garbuzov, Steve Zdancewic. CAV 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.
- Symbolic Analysis Tools for CSP, Liyi Li, Elsa L. Gunter, William Mansky. ICTAC 2014: 295-313
- A Cross-Language Framework for Verifying Compiler Optimizations, William Mansky, Elsa L. Gunter. Presented at LOLA 2014.
- Verifying Optimizations for Concurrent Programs, William Mansky, Elsa L. Gunter. WPTE@RTA/TLCA 2014: 15-26
- Specifying and Verifying Program Transformations with PTRANS, William Mansky. PhD thesis.
- Specifying and Executing Optimizations for Parallel Programs, William Mansky, Dennis Griffith, Elsa L. Gunter. GRAPHITE 2014: 58-70
- The PTRANS Specification Language, William Mansky. UIUC Technical Report, 2014.
- Using Locales to Define a Rely-Guarantee Temporal Logic, William Mansky, Elsa L. Gunter. ITP 2012: 299-314
- 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: 1817-1824
- A Framework for Formal Verification of Compiler Optimizations, William Mansky, Elsa L. Gunter. ITP 2010: 371-386