Synthesizing Imperative Programs from Examples Guided by Static Analysis
Abstract elided by the publisher.
783 papers · page 10 of 40
A Gradual Interpretation of Union Types
Union types allow to capture the possibility of a term to be of several possibly unrelated types. Traditional static approaches to union types are untagged and tagged unions, which present dual advantages in their use. Inspired by recent work on using abstract interpretation to u…
Modular Demand-Driven Analysis of Semantic Difference for Program Versions
Abstract elided by the publisher.
Incremental Analysis for Probabilistic Programs
Abstract elided by the publisher.
Automated Verification of Linearization Policies
Abstract elided by the publisher.
Simulation and Invariance for Weak Consistency
Abstract elided by the publisher.
Relational Verification Through Horn Clause Transformation
Abstract elided by the publisher.
Structure-Sensitive Points-To Analysis for C and C++
We present a points-to analysis for C/C++ that recovers much of the available high-level structure information of types and objects, by applying two key techniques: (1) It records the type of each abstract object and, in cases when the type is not readily available, the analysis …
Quantitative Monitor Automata
Abstract elided by the publisher.
Bounded Abstract Interpretation
Abstract elided by the publisher.
Securing a Compiler Transformation
Abstract elided by the publisher.
Enforcing Termination of Interprocedural Analysis
Abstract elided by the publisher.
Exploiting Sparsity in Difference-Bound Matrices
Abstract elided by the publisher.
Flow- and Context-Sensitive Points-To Analysis Using Generalized Points-To Graphs
Abstract elided by the publisher.
Learning a Variable-Clustering Strategy for Octagon from Labeled Data Generated by a Static Analysis
Abstract elided by the publisher.
Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Programs
Abstract elided by the publisher.
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
The template-based method is one of the most successful approaches to algebraic invariant synthesis. In this method, an algorithm designates a template polynomial \(p\) over program variables, generates constraints for \(p=0\) to be an invariant, and solves the generated constrai…
On the Linear Ranking Problem for Simple Floating-Point Loops
Abstract elided by the publisher.
Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM
Abstract elided by the publisher.
A Parametric Abstract Domain for Lattice-Valued Regular Expressions
Abstract elided by the publisher.