Complementation in Abstract Interpretation

ntation in Abstract Interpretation AGOSTINO CORTESI Universit`a di Venezia GILBERTO FIL´E Universit`a di Padova ROBERTO GIACOBAZZI Universit`a di Pisa CATUSCIA PALAMIDESSI Universit`a di Genova and FRANCESCO RANZATO Universit`a di Padova product of abstract domains is a rather well-known operation for domain composition act interpretation. In this article, we study its inverse operation, introducing a notion n complementation in abstract interpretation. Complementation provides a systematic esign new abstract domains, and it allows to systematically decompose domains. Also, such an operation allows to simplify domain verification problems, and it yields space-saving representations for complex domains. We show that the complement exists in most cases, and we mplementation to three well-known abstract domains, notably to Cousot and Cousot’s interval domain for integer variable analysis, to Cousot and Cousot’s domain for comportment analysis of functional languages, and to the doma...

• Type: Conference
• Year: 1995
• Where: SAS
• Authors: Agostino Cortesi, Gilberto Filé, Roberto Giacobazzi, Catuscia Palamidessi, Francesco Ranzato
• Keywords: Abstract Domain, Abstract Interpretation, Formal Methods, SAS 1995, Universit`a Di