enter search term and/or author name
A Master Theorem for Discrete Divide and Conquer Recurrences
Michael Drmota, Wojciech Szpankowski
Article No.: 16
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,...
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 W ⊆ V. 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
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
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...
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...
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency
Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
Article No.: 22
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...