REPT: Reverse Debugging of Failures in Deployed Software. - Weidong Cui; Xinyang Ge; Baris Kasikci; Ben Niu 007; Upamanyu Sharma; Ruoyu Wang 001; Insu Yun (OSDI, 2018)

Armada: low-effort verification of high-performance concurrent programs. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (PLDI, 2020)

Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Haojun Ma; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (ACM Trans. Program. Lang. Syst., 2022)

Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. - Yun-Sheng Chang; Ralf Jung 002; Upamanyu Sharma; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 2023)

Grove: a Separation-Logic Library for Verifying Distributed Systems. - Upamanyu Sharma; Ralf Jung 002; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (SOSP, 2023)

Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version). - Upamanyu Sharma; Ralf Jung 002; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (CoRR, 2023)

Performal: Formal Verification of Latency Properties for Distributed Systems. - Tony Nuda Zhang; Upamanyu Sharma; Manos Kapritsos (Proc. ACM Program. Lang., 2023)