Cell Morphing: From Array Programs to Array-Free Horn Clauses
Abstract elided by the publisher.
783 papers · page 11 of 40
Loopy: Programmable and Formally Verified Loop Transformations
Abstract elided by the publisher.
Completeness in Approximate Transduction
Abstract elided by the publisher.
Abstract Interpretation of Supermodular Games
Supermodular games are a well known class of noncooperative games which find significant applications in a variety of models, especially in operations research and economic applications. Supermodular games always have Nash equilibria which are characterized as fixed points of mul…
Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants
Abstract elided by the publisher.
The Julia Static Analyzer for Java
Abstract elided by the publisher.
From Array Domains to Abstract Interpretation Under Store-Buffer-Based Memory Models
Abstract elided by the publisher.
Making k-Object-Sensitive Pointer Analysis More Precise with Still k-Limiting
Object-sensitivity is regarded as arguably the best context abstraction for pointer analysis in object-oriented languages. However, a k-object-sensitive pointer analysis, which uses a sequence of k allocation sites (as k context elements) to represent a calling context of a metho…
Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization
While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachable sets, aka. the collecting semantics of the program. The verification of user-provided properties …
Parallel Cost Analysis of Distributed Systems
Abstract elided by the publisher.
May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization
Abstract elided by the publisher.
Static Analysis of Non-interference in Expressive Low-Level Languages
Abstract elided by the publisher.
A Forward Analysis for Recurrent Sets
Non-termination of structured imperative programs is primarily due to infinite loops. An important class of non-terminating loop behaviors can be characterized using the notion of recurrent sets. A recurrent set is a set of states from which execution of the loop cannot or might …
Safety Verification and Refutation by k-Invariants and k-Induction
Most software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexample generation in model checking, invariant inference in abstract interpretation and completeness via…
Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis
Abstract elided by the publisher.
Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration
Linear Time Invariant (LTI) systems are ubiquitous in software systems and control applications. Unbounded-time reachability analysis that can cope with industrial-scale models with thousands of variables is needed. To tackle this general problem, we use abstract acceleration, a …
A Binary Decision Tree Abstract Domain Functor
Abstract elided by the publisher.
SJS: A Type System for JavaScript with Fixed Object Layout
Abstract elided by the publisher.
Synthesizing Heap Manipulations via Integer Linear Programming
Abstract elided by the publisher.
Refinement Type Inference via Horn Constraint Optimization
We propose a novel method for inferring refinement types of higher-order functional programs. The main advantage of the proposed method is that it can infer maximally preferred (i.e., Pareto optimal) refinement types with respect to a user-specified preference order. The flexible…