Sciweavers

POPL
2016
ACM
8 years 18 days ago
Taming release-acquire consistency
We introduce a strengthening of the release-acquire fragment of the C11 memory model that (i) forbids dubious behaviors that are not observed in any implementation; (ii) supports ...
Ori Lahav, Nick Giannarakis, Viktor Vafeiadis
POPL
2016
ACM
8 years 18 days ago
Modelling the ARMv8 architecture, operationally: concurrency and ISA
In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). ...
Shaked Flur, Kathryn E. Gray, Christopher Pulte, S...
POPL
2016
ACM
8 years 18 days ago
Newtonian program analysis via tensor product
Recently, Esparza et al. generalized Newton’s method—a numerical-analysis algorithm for finding roots of real-valued functions—to a method for finding fixed-points of sys...
Thomas W. Reps, Emma Turetsky, Prathmesh Prabhu
POPL
2016
ACM
8 years 18 days ago
Learning invariants using decision trees and implication counterexamples
Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations...
Pranav Garg 0001, Daniel Neider, P. Madhusudan, Da...
POPL
2016
ACM
8 years 18 days ago
Is sound gradual typing dead?
Programmers have come to embrace dynamically-typed languages for prototyping and delivering large and complex systems. When it comes to maintaining and evolving these systems, the...
Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S...
POPL
2016
ACM
8 years 18 days ago
Symbolic computation of differential equivalences
Ordinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and ele...
Luca Cardelli, Mirco Tribastone, Max Tschaikowski,...
POPL
2016
ACM
8 years 18 days ago
From MinX to MinC: semantics-driven decompilation of recursive datatypes
Reconstructing the meaning of a program from its binary executable is known as reverse engineering; it has a wide range of applications in software security, exposing piracy, lega...
Edward Robbins, Andy King, Tom Schrijvers
POPL
2016
ACM
8 years 18 days ago
Kleenex: compiling nondeterministic transducers to deterministic streaming transducers
We present and illustrate Kleenex, a language for expressing general nondeterministic finite transducers, and its novel compilation to streaming string transducers with worst-cas...
Niels Bjørn Bugge Grathwohl, Fritz Henglein...
POPL
2016
ACM
8 years 18 days ago
Estimating types in binaries using predictive modeling
Reverse engineering is an important tool in mitigating vulnerabilities in binaries. As a lot of software is developed in object-oriented languages, reverse engineering of object-o...
Omer Katz, Ran El-Yaniv, Eran Yahav
POPL
2016
ACM
8 years 18 days ago
Decidability of inferring inductive invariants
Induction is a successful approach for verification of hardware and software systems. A common practice is to model a system using logical formulas, and then use a decision proce...
Oded Padon, Neil Immerman, Sharon Shoham, Aleksand...