17 citations · 18 across the 5 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
Relational verification encompasses research directions such as reasoning about data abstraction, reasoning about security and privacy, secure compilation, and functional specifica…
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…