Sciweavers

POPL
2016
ACM
8 years 7 months ago
Model checking for symbolic-heap separation logic with inductive predicates
We investigate the model checking problem for symbolic-heap separation logic with user-defined inductive predicates, i.e., the problem of checking that a given stack-heap memory ...
James Brotherston, Nikos Gorogiannis, Max I. Kanov...
POPL
2016
ACM
8 years 7 months ago
Printing floating-point numbers: a faster, always correct method
Floating-point numbers are an essential part of modern software, recently gaining particular prominence on the web as the exclusive numeric format of Javascript. To use floating-...
Marc Andrysco, Ranjit Jhala, Sorin Lerner
POPL
2016
ACM
8 years 7 months ago
Optimizing synthesis with metasketches
Many advanced programming tools—for both end-users and expert developers—rely on program synthesis to automatically generate implementations from high-level specifications. T...
James Bornholt, Emina Torlak, Dan Grossman, Luis C...
POPL
2016
ACM
8 years 7 months ago
String solving with word equations and transducers: towards a logic for analysing mutation XSS
We study the fundamental issue of decidability of satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting t...
Anthony Widjaja Lin, Pablo Barceló
POPL
2016
ACM
8 years 7 months ago
Fully-abstract compilation by approximate back-translation
Dominique Devriese, Marco Patrignani, Frank Piesse...
POPL
2016
ACM
8 years 7 months ago
Overhauling SC atomics in c11 and OpenCL
Despite the conceptual simplicity of sequential consistency (SC), the semantics of SC atomic operations and fences in the C11 and OpenCL memory models is subtle, leading to convol...
Mark Batty, Alastair F. Donaldson, John Wickerson
POPL
2016
ACM
8 years 7 months ago
A program logic for concurrent objects under fair scheduling
Existing work on verifying concurrent objects is mostly concerned with safety only, e.g., partial correctness or linearizability. Although there has been recent work verifying loc...
Hongjin Liang, Xinyu Feng
POPL
2016
ACM
8 years 7 months ago
'Cause I'm strong enough: reasoning about consistency choices in distributed systems
Large-scale distributed systems often rely on replicated databases that allow a programmer to request different data consistency guarantees for different operations, and thereby c...
Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mah...
POPL
2016
ACM
8 years 7 months ago
Learning programs from noisy data
We present a new approach for learning programs from noisy datasets. Our approach is based on two new concepts: a regularized program generator which produces a candidate program ...
Veselin Raychev, Pavol Bielik, Martin T. Vechev, A...