hide
Free keywords:
-
Abstract:
The goal of this paper is to illustrate the wide applicability
in verification of results on local reasoning, and especially
on hierarchical reasoning in local theory extensions.
The paper contains a survey of our results on reasoning in
local theory extensions, ranging from characterizations of
locality to interpolation. In addition, several examples are
provided, emphasizing theories occurring in a natural way in
verification. We give several examples -- some already
existing in the literature, others obtained during the work
in the AVACS project -- of application domains where such
theories occur in a natural way.
