enter search term and/or author name
Dependent Type Theory for Verification of Information Flow and Access Control Policies
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
Article No.: 6
Dedicated to the memory of John C. Reynolds (1935--2013).
We present Relational Hoare Type Theory (RHTT), a novel language and verification system capable of expressing and verifying rich information flow and access control policies via...
Several authors have found evidence of large dependence clusters in the source code of a diverse range of systems, domains, and programming languages. This raises the question of how we might efficiently locate the fragments of code that give rise...
Proof-Directed Parallelization Synthesis by Separation Logic
Matko Botinčan, Mike Dodds, Suresh Jagannathan
Article No.: 8
We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, written in separation logic, and produces a correctly synchronized...