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.

Deriving Bisimulations by Simplifying Partitions

MASTROENI, Isabella
2008-01-01

Abstract

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.
2008
9783540781622
Abstract interpretation; Bisimulation; Partition refining
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/313571
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 3
social impact