A Kleene analysis of Mobile Ambients

Flemming Nielson, Hanne Riis Nielson, M. Sagiv

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


    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.
    Original languageEnglish
    Title of host publicationProc. ESOP'00
    PublisherSpringer Verlag
    Publication date2000
    Publication statusPublished - 2000
    EventProc. ESOP'00 -
    Duration: 1 Jan 2000 → …


    ConferenceProc. ESOP'00
    Period01/01/2000 → …


    Dive into the research topics of 'A Kleene analysis of Mobile Ambients'. Together they form a unique fingerprint.

    Cite this