On local reasoning in verification

theories important in verification for which efficient reasoning
methods exist. The framework we present is based on a general
notion of locality. We show that locality considerations allow
us to obtain parameterized decidability and complexity results for
many (combinations of) theories important in verification in
general and in the verification of parametric systems in particular.

We give numerous examples: in particular we show that several
theories of data structures studied in the verification literature
are local extensions of a base theory. The general framework we use
allows us to identify situations in which some of the syntactical
restrictions imposed in previous papers can be relaxed.

(joint work with Carsten Ihlemann and Swen Jacobs)