7 citations · 18 across the 17 of their papers we have counts for
19 papers
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 (…
Formally Verified Samplers From Probabilistic Programs With Loops and Conditioning
Alexander Bagnall, Gordon Stewart, Anindya Banerjee
We present Zar: a formally verified compiler pipeline from discrete probabilistic programs with unbounded loops in the conditional probabilistic guarded command language (cpGCL) to…
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee +2
Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that…
Hyperkähler Isometries Of K3 Surfaces
Anindya Banerjee, Gregory W. Moore
We consider symmetries of K3 manifolds. Holomorphic symplectic automorphisms of K3 surfaces have been classified, and observed to be subgroups of the Mathieu group . More r…
Verification of ML Systems via Reparameterization
Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha +2
As machine learning is increasingly used in essential systems, it is important to reduce or eliminate the incidence of serious bugs. A growing body of research has developed machin…