In this paper we analyze the problem of transforming partitions in order to satisfy completeness in the standard abstract interpretation framework. By using the straightforward characterization of equivalence relations by means of abstract domains, we instantiate the framework for making abstract domains complete to partitions. In order to obtain this, we exploit the relation existing between completeness and the Paige-Tarjan notion of stability, already detected in the particular context of refining partitions for completeness. Here we extend this relation in order to cope not only with both the existing notions of completeness, but also with the simplification of domains for completeness (the so called core). Then we show that completeness is present under the stability form, in two fields of computer science security: abstract non-interference and opacity.
File in questo prodotto:
Non ci sono file associati a questo prodotto.