| A formal C memory model supporting integer-pointer casts J Kang, CK Hur, W Mansky, D Garbuzov, S Zdancewic, V Vafeiadis Proceedings of the 36th ACM SIGPLAN Conference on Programming Language …, 2015 | 70 | 2015 |
| From C to interaction trees: specifying, verifying, and testing a networked server N Koh, Y Li, Y Li, L Xia, L Beringer, W Honoré, W Mansky, BC Pierce, ... Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 62 | 2019 |
| A framework for formal verification of compiler optimizations W Mansky, E Gunter Interactive Theorem Proving: First International Conference, ITP 2010 …, 2010 | 46 | 2010 |
| Toward a multi-method approach to formalizing human-automation interaction and human-human communications EJ Bass, ML Bolton, K Feigh, D Griffith, E Gunter, W Mansky, J Rushby 2011 IEEE International Conference on Systems, Man, and Cybernetics, 1817-1824, 2011 | 44 | 2011 |
| BARRACUDA: binary-level analysis of runtime RAces in CUDA programs A Eizenberg, Y Peng, T Pigli, W Mansky, J Devietti Proceedings of the 38th ACM SIGPLAN Conference on Programming Language …, 2017 | 37 | 2017 |
| Verifying an HTTP key-value server with Interaction Trees and VST H Zhang, W Honoré, N Koh, Y Li, Y Li, LY Xia, L Beringer, W Mansky, ... 12th International Conference on Interactive Theorem Proving (ITP 2021), 2021 | 31 | 2021 |
| A verified messaging system W Mansky, AW Appel, A Nogin Proceedings of the ACM on Programming Languages 1 (OOPSLA), 1-28, 2017 | 29 | 2017 |
| Compass: strong and compositional library specifications in relaxed memory separation logic HH Dang, J Jung, J Choi, DT Nguyen, W Mansky, J Kang, D Dreyer Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022 | 21 | 2022 |
| Connecting Higher-Order Separation Logic to a First-Order Outside World W Mansky, W Honoré, AW Appel European Symposium on Programming, 428-455, 2020 | 19 | 2020 |
| An axiomatic specification for sequential memory models W Mansky, D Garbuzov, S Zdancewic Computer Aided Verification: 27th International Conference, CAV 2015, San …, 2015 | 19 | 2015 |
| Verifying dynamic race detection W Mansky, Y Peng, S Zdancewic, J Devietti Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 16 | 2017 |
| Specifying and verifying program transformations with PTRANS W Mansky University of Illinois at Urbana-Champaign, 2014 | 11 | 2014 |
| SLIMFAST: Reducing Metadata Redundancy in Sound and Complete Dynamic Data Race Detection Y Peng, C DeLozier, A Eizenberg, W Mansky, J Devietti 2018 IEEE International Parallel and Distributed Processing Symposium (IPDPS …, 2018 | 10 | 2018 |
| Compiler Correctness for Concurrency: from concurrent separation logic to shared-memory assembly language S Cuellar, N Giannarakis, JM Madiot, W Mansky, L Beringer, Q Cao, ... Technical Report TBD, Department of Computer Science, Princeton University, 2020 | 9 | 2020 |
| Specifying and executing optimizations for generalized control flow graphs W Mansky, EL Gunter, D Griffith, MD Adams Science of Computer Programming 130, 2-23, 2016 | 8 | 2016 |
| Bringing Iris into the Verified Software Toolchain W Mansky arXiv preprint arXiv:2207.06574, 2022 | 6 | 2022 |
| Verifying optimizations for concurrent programs W Mansky, EL Gunter First International Workshop on Rewriting Techniques for Program …, 2014 | 6 | 2014 |
| Specifying and executing optimizations for parallel programs W Mansky, D Griffith, EL Gunter arXiv preprint arXiv:1407.7932, 2014 | 4 | 2014 |
| Using locales to define a rely-guarantee temporal logic W Mansky, EL Gunter Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 4 | 2012 |
| Automating separation logic for Concurrent C minor W Mansky Undergraduate thesis (May 2008), 2008 | 4 | 2008 |
Steve ZdancewicProfessor of Computer and Information Science, University of Pennsylvania在 cis.upenn.edu 的电子邮件经过验证
