Journal of the ACM (JACM)


Search Issue
enter search term and/or author name


Journal of the ACM (JACM), Volume 60 Issue 3, June 2013

A Master Theorem for Discrete Divide and Conquer Recurrences
Michael Drmota, Wojciech Szpankowski
Article No.: 16
DOI: 10.1145/2487241.2487242

Divide-and-conquer recurrences are one of the most studied equations in computer science. Yet, discrete versions of these recurrences, namely for some known sequence an and given bj, bj,...

The VPN Conjecture Is True
Navin Goyal, Neil Olver, F. Bruce Shepherd
Article No.: 17
DOI: 10.1145/2487241.2487243

We consider the following network design problem. We are given an undirected graph G = (V,E) with edge costs c(e) and a set of terminal nodes WV. A hose demand matrix is any symmetric...

Local Reasoning for Global Invariants, Part I: Region Logic
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Article No.: 18
DOI: 10.1145/2485982

Dedicated to the memory of Stephen L. Bloom (1940--2010).

Shared mutable objects pose grave challenges in reasoning, especially for information hiding and modularity. This article presents a novel technique for reasoning about...

Local Reasoning for Global Invariants, Part II: Dynamic Boundaries
Anindya Banerjee, David A. Naumann
Article No.: 19
DOI: 10.1145/2485981

Dedicated to the memory of John C. Reynolds (1935--2013).

The hiding of internal invariants creates a mismatch between procedure specifications in an interface and proof obligations on the implementations of those procedures. The mismatch...

Model Checking Higher-Order Programs
Naoki Kobayashi
Article No.: 20
DOI: 10.1145/2487241.2487246

We propose a novel verification method for higher-order functional programs based on higher-order model checking, or more precisely, model checking of higher-order recursion schemes (recursion schemes, for short). The most distinguishing feature...

Invited Article Foreword
Victor Vianu
Article No.: 21
DOI: 10.1145/2487241.2487247

CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency
Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
Article No.: 22
DOI: 10.1145/2487241.2487248

In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several...