Sciweavers

Share
ESOP
2000
Springer

A Kleene Analysis of Mobile Ambients

9 years 11 months ago
A Kleene Analysis of Mobile Ambients
Abstract. We show how a program analysis technique originally developed for C-like pointer structures can be adapted to analyse the hierarchical structure of processes in the ambient calculus. The technique is based on modeling the semantics of the language in a two-valued logic; by reinterpreting the logical formulae in Kleene's three-valued logic we obtain an analysis allowing us to reason about may as well as must properties. The correctness of the approach follows from a general Embedding Theorem for Kleene's logic; furthermore embeddings allow us to reduce the size of structures so as to control the time and space complexity of the analysis.
Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where ESOP
Authors Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv
Comments (0)
books