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.

• Type: Conference
• Year: 2000
• Where: ESOP
• Authors: Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv
• Keywords: C-like Pointer Structures, ESOP 2000, Kleene's Three-valued Logic, Program Analysis Technique, Programming Languages