This paper addresses the problem of proving a given invariance property phi of a loop in a numeric program, by inferring automatically a stronger inductive invariant psi. The algorithm we present is based on both abstract ...

In 1979, Cousot and Cousot gave a specification of the ?best? (most-precise) abstract transformer possible for a given concrete transformer and a given abstract domain. Unfortunately, their specification does not lead to ...

This paper considers some known abstract domains for affine-relation analysis, along with several variants, and studies how they relate to each other. The various domains represent sets of points that satisfy affine ...

In abstract interpretation, the choice of an abstract domain fixes a limit on the precision of the inductive invariants that one can express; however, for a given abstract domain A, there is a most-precise (``strongest'', ...

This paper advances the state of the art in abstract interpretation of machine code. It tackles two of the biggest challenges in machine-code analysis: (1) holding onto invariants about values in memory, and (2) identifying ...

Given a concrete domain C, a concrete operation tau: C -> C, and an abstract domain A, a fundamental problem in abstract interpretation is to find the best abstract transformer tau#: A -> A that over-approximates tau. ...

This paper gives an account of Staalmarck's method for validity checking of propositional-logic formulas, and explains each of the key components in terms of concepts from the field of abstract interpretation. We then ...

Abstract. This paper addresses the problem of abstracting a set of affine transformers v' = v C + d, where v and v' represent the pre-state and post-state, respectively. We introduce a framework to harness any base abstract ...

This dissertation explores the use of abstraction in two areas of automated reasoning: verification of programs, and decision procedures for logics. Establishing that a program is correct is undecidable in general. ...

Separation logic is an expressive logic for reasoning about heap structures in programs. This paper presents a semi-decision procedure for checking unsatisfiability of formulas in a fragment of separation logic that includes ...