Campus Event Calendar
Event Entry
What and Who
Reasoning about Arrays
Aaron Bradley
Stanford University
Avacs Virtual Seminar
AG 1, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 30 November 2007
13:30
45 Minutes
E1 4
024
Saarbrücken
Abstract
Arrays are a basic data structure in imperative programs and hardware.
John McCarthy formalized arrays as a first-order theory in 1962. All
modern SMT (Satisfiability Modulo Theories) solvers can decide
satisfiability of quantifier-free array formulae based on a decision
procedure first implemented by James King in 1969. However, the
quantifier-free fragment can only express information about a finite
number of positions of arrays --- those positions that a formula
explicitly references. Expressing constraints about segments of
arrays requires either augmenting the theory with extra predicates or
considering formulae with at least one quantifier alternation. The
former approach was taken in a series of studies in the 1980s (Suzuki,
Jefferson; Jaffar; Mateti) and then again in 2001 (Stump, Barrett,
Dill, Levitt); they focus on quantifier-free fragments of theories
augmented with predicates such as "sorted", "partitioned", and
equality between arrays.
In joint work with Zohar Manna and Henny Sipma, I took the latter
approach. I will describe the "array property fragments" of theories
of arrays with integer indices (standard imperative arrays) and with
uninterpreted indices ("maps"). Because formulae of the fragments can
have one (limited) quantifier alternation, they allow encoding the
various predicates that were previously studied in isolation, as well
as other properties. The array property fragment of maps is also
useful for modeling sets, multisets, and hashtables. After presenting
simple decision procedures based on quantifier instantiation (which
have been implemented in several SMT solvers), I will show that each
of several obvious and natural extensions to the fragments makes
satisfiability undecidable.
The presentation is based on Chapter 2 of my PhD thesis, which is
available online at http://theory.stanford.edu/~arbrad
<http://theory.stanford.edu/%7Earbrad>.
John McCarthy formalized arrays as a first-order theory in 1962. All
modern SMT (Satisfiability Modulo Theories) solvers can decide
satisfiability of quantifier-free array formulae based on a decision
procedure first implemented by James King in 1969. However, the
quantifier-free fragment can only express information about a finite
number of positions of arrays --- those positions that a formula
explicitly references. Expressing constraints about segments of
arrays requires either augmenting the theory with extra predicates or
considering formulae with at least one quantifier alternation. The
former approach was taken in a series of studies in the 1980s (Suzuki,
Jefferson; Jaffar; Mateti) and then again in 2001 (Stump, Barrett,
Dill, Levitt); they focus on quantifier-free fragments of theories
augmented with predicates such as "sorted", "partitioned", and
equality between arrays.
In joint work with Zohar Manna and Henny Sipma, I took the latter
approach. I will describe the "array property fragments" of theories
of arrays with integer indices (standard imperative arrays) and with
uninterpreted indices ("maps"). Because formulae of the fragments can
have one (limited) quantifier alternation, they allow encoding the
various predicates that were previously studied in isolation, as well
as other properties. The array property fragment of maps is also
useful for modeling sets, multisets, and hashtables. After presenting
simple decision procedures based on quantifier instantiation (which
have been implemented in several SMT solvers), I will show that each
of several obvious and natural extensions to the fragments makes
satisfiability undecidable.
The presentation is based on Chapter 2 of my PhD thesis, which is
available online at http://theory.stanford.edu/~arbrad
<http://theory.stanford.edu/%7Earbrad>.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 11/27/2007 16:39 -- Created document.