25 citations · 50 across the 16 of their papers we have counts for
5 papers · 1 filter
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…
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
Mounir Assaf, David A. Naumann, Julien Signoles +2
We show how static analysis for secure information flow can be expressed and proved correct entirely within the framework of abstract interpretation. The key idea is to define a Ga…
Towards Patterns for Heaps and Imperative Lambdas
David A. Naumann
In functional programming, point-free relation calculi have been fruitful for general theories of program construction, but for specific applications pointwise expressions can be m…
A Simple Semantics and Static Analysis for Stack Inspection
Anindya Banerjee, David A. Naumann
The Java virtual machine and the .NET common language runtime feature an access control mechanism specified operationally in terms of run-time stack inspection. We give a denotatio…
Ownership Confinement Ensures Representation Independence for Object-Oriented Programs
Anindya Banerjee, David A. Naumann
Dedicated to the memory of Edsger W.Dijkstra. Representation independence or relational parametricity formally characterizes the encapsulation provided by language constructs for d…