Sciweavers

POPL
2015
ACM
8 years 7 months ago
Analyzing Program Analyses
We want to prove that a static analysis of a given program is complete, namely, no imprecision arises when asking some query on the program behavior in the concrete (i.e., for its...
Roberto Giacobazzi, Francesco Logozzo, Francesco R...
POPL
2015
ACM
8 years 7 months ago
Predicting Program Properties from "Big Code"
We present a new approach for predicting program properties from massive codebases (aka “Big Code”). Our approach first learns a probabilistic model from existing data and th...
Veselin Raychev, Martin T. Vechev, Andreas Krause
POPL
2015
ACM
8 years 7 months ago
A Calculus for Relaxed Memory
We propose a new approach to programming multi-core, relaxed-memory architectures in imperative, portable programming languages. Our memory model is based on explicit, programmer-...
Karl Crary, Michael J. Sullivan
POPL
2015
ACM
8 years 7 months ago
Ur/Web: A Simple Model for Programming the Web
The World Wide Web has evolved gradually from a document delivery platform to an architecture for distributed programming. This largely unplanned evolution is apparent in the set ...
Adam Chlipala
POPL
2015
ACM
8 years 7 months ago
A Scalable, Correct Time-Stamped Stack
Concurrent data-structures, such as stacks, queues, and deques, often implicitly enforce a total order over elements in their underlying memory layout. However, much of this order...
Mike Dodds, Andreas Haas, Christoph M. Kirsch
POPL
2015
ACM
8 years 7 months ago
Decentralizing SDN Policies
Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logicallycentralized control over network devices through a “contr...
Oded Padon, Neil Immerman, Aleksandr Karbyshev, Or...
POPL
2015
ACM
8 years 7 months ago
Proof Spaces for Unbounded Parallelism
In this paper, we present a new approach to automatically verify multi-threaded programs which are executed by an unbounded number of threads running in parallel. The starting poi...
Azadeh Farzan, Zachary Kincaid, Andreas Podelski
POPL
2015
ACM
8 years 7 months ago
Differential Privacy: Now it's Getting Personal
Differential privacy provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties...
Hamid Ebadi, David Sands, Gerardo Schneider
POPL
2015
ACM
8 years 7 months ago
Self-Representation in Girard's System U
In 1991, Pfenning and Lee studied whether System F could support a typed self-interpreter. They concluded that typed selfrepresentation for System F “seems to be impossible”, ...
Matt Brown, Jens Palsberg
POPL
2015
ACM
8 years 7 months ago
Manifest Contracts for Datatypes
We study algebraic datatypes in a manifest contract system, a software contract system where contract information occurs as refinement types. We first compare two simple approac...
Taro Sekiyama, Yuki Nishida, Atsushi Igarashi