Data Abstraction and Relational Program Logic. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann; Mohammad Nikouei (CoRR, 2019)

Alignment Completeness for Relational Hoare Logics. - Ramana Nagasamudram; David A. Naumann (LICS, 2021)

Making Relational Hoare Logic Alignment Complete. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann (CoRR, 2022)

A Relational Program Logic with Data Abstraction and Dynamic Framing. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann; Mohammad Nikouei (ACM Trans. Program. Lang. Syst., 2022)

The WhyRel Prototype for Modular Relational Verification of Pointer Programs. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (TACAS (2), 2023)

The WhyRel Prototype for Relational Verification. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (CoRR, 2023)

Alignment complete relational Hoare logics for some and all. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (CoRR, 2023)

An Algebra of Alignment for Relational Verification. - Timos Antonopoulos; Eric Koskinen; Ton Chanh Le; Ramana Nagasamudram; David A. Naumann; Minh Ngo (Proc. ACM Program. Lang., 2023)

Verifying a C Implementation of Derecho's Coordination Mechanism Using VST and Coq. - Ramana Nagasamudram; Lennart Beringer; Ken Birman; Mae Milano; David A. Naumann (NFM, 2024)

Verifying a C implementation of Derecho's coordination mechanism using VST and Coq (artifact). - Ramana Nagasamudram; Lennart Beringer; Ken Birman; Mae Milano; David A. Naumann (Zenodo, 2024)