ACM DL

Programming Languages and Systems (TOPLAS)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 35 Issue 2, July 2013

Dependent Type Theory for Verification of Information Flow and Access Control Policies
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
Article No.: 6
DOI: 10.1145/2491522.2491523

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...

Efficient Identification of Linchpin Vertices in Dependence Clusters
David Binkley, Nicolas Gold, Mark Harman, Syed Islam, Jens Krinke, Zheng Li
Article No.: 7
DOI: 10.1145/2491522.2491524

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
DOI: 10.1145/2491522.2491525

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...