| {BesFS}: A {POSIX} Filesystem for Enclaves with a Mechanized Safety Proof S Shinde, S Wang, P Yuan, A Hobor, A Roychoudhury, P Saxena 29th USENIX Security Symposium (USENIX Security 20), 523-540, 2020 | 28 | 2020 |
| Certifying graph-manipulating C programs via localizations within data structures S Wang, Q Cao, A Mohan, A Hobor Proceedings of the ACM on Programming Languages 3 (OOPSLA), 1-30, 2019 | 25 | 2019 |
| Besfs: Mechanized proof of an iago-safe filesystem for enclaves S Shinde, S Wang, P Yuan, A Hobor, A Roychoudhury, P Saxena ArXiv e-prints, 2018 | 9 | 2018 |
| Certified reasoning with infinity A Sharma, S Wang, A Costea, A Hobor, WN Chin FM 2015: Formal Methods: 20th International Symposium, Oslo, Norway, June 24 …, 2015 | 7 | 2015 |
| Proof Pearl: Magic Wand as Frame Q Cao, S Wang, A Hobor, AW Appel arXiv preprint arXiv:1909.08789, 2019 | 5 | 2019 |
| Proof pearl: Magic wand as frame Q Cao, S Wang, A Hobor, AW Appel Unpublished, 2018 | 5 | 2018 |
| Compositional verification of concurrent C programs with search structure templates DT Nguyen, L Beringer, W Mansky, S Wang Proceedings of the 13th ACM SIGPLAN International Conference on Certified …, 2024 | 3 | 2024 |
| Foundational verification of stateful P4 packet processing Q Wang, M Pan, S Wang, R Doenges, L Beringer, AW Appel 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 | 3 | 2023 |
| Stack bound inference for abstract java bytecode S Wang, Z Qiu, S Qin, WN Chin 2010 4th IEEE International Symposium on Theoretical Aspects of Software …, 2010 | 3 | 2010 |
| Proving Logical Atomicity using Lock Invariants R Sharma, S Wang, A Oey, A Evdokimova, L Beringer, W Mansky arXiv preprint arXiv:2304.13898, 2023 | 1 | 2023 |
| A Machine-Checked C Implementation of Dijkstra’s Shortest Path Algorithm A Mohan, S Wang, A Hobor | | |
| The Ramifications of Mechanized Localizations within Data Structures SWQCA Sharma, X Aquinas Hobor | | |
