William Mansky

According to our database, William Mansky authored at least 23 papers between 2010 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

An Iris Instance for Verifying CompCert C Programs.

William Mansky, Ke Du

Proc. ACM Program. Lang., January, 2024

Compositional Verification of Concurrent C Programs with Search Structure Templates.

Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Proving Logical Atomicity using Lock Invariants.

Roshan Sharma, Shengyi Wang, Alexander Oey, Anastasiia Evdokimova, Lennart Beringer, William Mansky

CoRR, 2023

2022

Bringing Iris into the Verified Software Toolchain.

William Mansky

CoRR, 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

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

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 C. Pierce, Steve Zdancewic

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020

Connecting Higher-Order Separation Logic to a First-Order Outside World.

William Mansky, Wolf Honoré, Andrew W. Appel

Proceedings of the Programming Languages and Systems, 2020

2019

From C to interaction trees: specifying, verifying, and testing a networked server.

Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Structural Operational Semantics for Control Flow Graph Machines.

Dmitri Garbuzov, William Mansky, Christine Rizkallah, Steve Zdancewic

CoRR, 2018

SLIMFAST: Reducing Metadata Redundancy in Sound and Complete Dynamic Data Race Detection.

Yuanfeng Peng, Christian DeLozier, Ariel Eizenberg, William Mansky, Joseph Devietti

Proceedings of the 2018 IEEE International Parallel and Distributed Processing Symposium, 2018

2017

A verified messaging system.

William Mansky, Andrew W. Appel, Aleksey Nogin

Proc. ACM Program. Lang., 2017

BARRACUDA: binary-level analysis of runtime RAces in CUDA programs.

Ariel Eizenberg, Yuanfeng Peng, Toma Pigli, William Mansky, Joseph Devietti

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Verifying dynamic race detection.

William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Specifying and executing optimizations for generalized control flow graphs.

William Mansky, Elsa L. Gunter, Dennis Griffith, Michael D. Adams

Sci. Comput. Program., 2016

2015

A formal C memory model supporting integer-pointer casts.

Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

An Axiomatic Specification for Sequential Memory Models.

William Mansky, Dmitri Garbuzov, Steve Zdancewic

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Specifying and verifying program transformations with PTRANS

William Mansky

PhD thesis, 2014

Specifying and Executing Optimizations for Parallel Programs.

William Mansky, Dennis Griffith, Elsa L. Gunter

Proceedings of the Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering, 2014

Verifying Optimizations for Concurrent Programs.

William Mansky, Elsa L. Gunter

Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2014

Symbolic Analysis Tools for CSP.

Liyi Li, Elsa L. Gunter, William Mansky

Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

2012

Using Locales to Define a Rely-Guarantee Temporal Logic.

William Mansky, Elsa L. Gunter

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

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

Proceedings of the IEEE International Conference on Systems, 2011

2010

A Framework for Formal Verification of Compiler Optimizations.

William Mansky, Elsa L. Gunter

Proceedings of the Interactive Theorem Proving, First International Conference, 2010