25 citations · 50 across the 16 of their papers we have counts for
17 papers
Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI
David A. Naumann
Many high-level security requirements are about the allowed flow of information in programs and are difficult to make precise because they involve selective downgrading. Notions fr…
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…