17 citations · 19 across the 6 of their papers we have counts for
7 papers
Forall-Exists Relational Verification by Filtering to Forall-Forall
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann +1
Relational verification encompasses reasoning about data abstraction, security and privacy, secure compilation, and functional specification of tensor programs, among others. Sever…
Alignment complete relational Hoare logics for some and all
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (…
The WhyRel Prototype for Relational Verification
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (re…
Making Relational Hoare Logic Alignment Complete
Anindya Banerjee, Ramana Nagasamudram, David A. Naumann
In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (…
An algebra of alignment for relational verification
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le +3
Relational verification encompasses information flow security, regression verification, translation validation for compilers, and more. Effective alignment of the programs and comp…
Alignment Completeness for Relational Hoare Logics
Ramana Nagasamudram, David A. Naumann
Relational Hoare logics (RHL) provide rules for reasoning about relations between programs. Several RHLs include a rule we call sequential product that infers a relational correctn…
A Relational Program Logic with Data Abstraction and Dynamic Framing
Anindya Banerjee, Ramana Nagasamudram, David A. Naumann +1
Dedicated to Tony Hoare. In a paper published in 1972 Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data repres…