Synthesis of Memory Fences via Refinement Propagation
Abstract elided by the publisher.
783 papers · page 13 of 40
Abstract elided by the publisher.
Abstract elided by the publisher.
We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and c…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
We propose a new approach to heap analysis through an abstract domain of automata, called automatic shapes. Automatic shapes are modeled after a particular version of quantified data automata on skinny trees (QSDAs), that allows to define universally quantified properties of prog…
Abstract elided by the publisher.
Abstract elided by the publisher.
Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone.
Abstract elided by the publisher.
This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce λ Actor, a prototypical functional language with pattern-matching algebraic data types, augmented with process creati…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a …
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.