Sciweavers

PLDI
2015
ACM
8 years 11 days ago
Automatically improving accuracy for floating point expressions
Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate to...
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilc...
PLDI
2015
ACM
8 years 11 days ago
Provably correct peephole optimizations with alive
Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. These optim...
Nuno P. Lopes, David Menendez, Santosh Nagarakatte...
PLDI
2015
ACM
8 years 11 days ago
Sound reasoning about integral data types with a reusable SMT solver interface
We extend the Leon verification system for Scala with support for bitvector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment o...
Régis Blanc, Viktor Kuncak
PLDI
2015
ACM
8 years 11 days ago
Many-core compiler fuzzing
We address the compiler correctness problem for many-core systems through novel applications of fuzz testing to OpenCL compilers. Focusing on two methods from prior work, random d...
Christopher Lidbury, Andrei Lascu, Nathan Chong, A...
PLDI
2015
ACM
8 years 11 days ago
The Push/Pull model of transactions
We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics...
Eric Koskinen, Matthew J. Parkinson
PLDI
2015
ACM
8 years 11 days ago
Lightweight, flexible object-oriented generics
The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanis...
Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi...
PLDI
2015
ACM
8 years 11 days ago
Automatic induction proofs of data-structures in imperative programs
We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose definitions are formalized via ...
Duc-Hiep Chu, Joxan Jaffar, Minh-Thai Trinh
PLDI
2015
ACM
8 years 11 days ago
Blame and coercion: together again for the first time
Jeremy G. Siek, Peter Thiemann, Philip Wadler
PLDI
2015
ACM
8 years 11 days ago
SnapQueue: lock-free queue with constant time snapshots
We introduce SnapQueues - concurrent, lock-free queues with a linearizable, lock-free global-state transition operation. This transition operation can atomically switch between ar...
Aleksandar Prokopec