Synthesis of Memory Fences via Refinement Propagation
Abstract elided by the publisher.
783 papers · page 13 of 40
Speeding Up Logico-Numerical Strategy Iteration
Abstract elided by the publisher.
Cost-Aware Automatic Program Repair
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…
An Abstract Domain Combinator for Separately Conjoining Memory Abstractions
Abstract elided by the publisher.
A Decision Tree Abstract Domain for Proving Conditional Termination
Abstract elided by the publisher.
Region-Based Selective Flow-Sensitive Pointer Analysis
Abstract elided by the publisher.
Verification as Learning Geometric Concepts
Abstract elided by the publisher.
Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists
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…
Localizing Widening and Narrowing
Abstract elided by the publisher.
On Solving Universally Quantified Horn Clauses
Abstract elided by the publisher.
Formal Verification of a C Value Analysis Based on Abstract Interpretation
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.
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL
Abstract elided by the publisher.
Automatic Verification of Erlang-Style Concurrency
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…
Predicate Abstraction for Relaxed Memory Models
Abstract elided by the publisher.
Local Shape Analysis for Overlaid Data Structures
Abstract elided by the publisher.
Byte-Precise Verification of Low-Level List Manipulation
Abstract elided by the publisher.
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra
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 Interpretation over Non-lattice Abstract Domains
Abstract elided by the publisher.
Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT
Abstract elided by the publisher.
Static Validation of Dynamically Generated HTML Documents Based on Abstract Parsing and Semantic Processing
Abstract elided by the publisher.