A Kleene analysis of Mobile Ambients

Flemming Nielson; Hanne Riis Nielson; M. Sagiv

A Kleene analysis of Mobile Ambients

Flemming Nielson, Hanne Riis Nielson, M. Sagiv

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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.

Original language	English
Title of host publication	Proc. ESOP'00
Publisher	Springer Verlag
Publication date	2000
Pages	305-319
Publication status	Published - 2000
Event	Proc. ESOP'00 - Duration: 1 Jan 2000 → …

Conference

Conference	Proc. ESOP'00
Period	01/01/2000 → …

OpenUrl availability

Full text

Cite this

@inproceedings{36b187eda5bb4b41974864638be0c1a8,

title = "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.",

author = "Flemming Nielson and Nielson, \{Hanne Riis\} and M. Sagiv",

year = "2000",

language = "English",

pages = "305--319",

booktitle = "Proc. ESOP'00",

publisher = "Springer Verlag",

address = "Germany",

note = "Proc. ESOP'00 ; Conference date: 01-01-2000",

}

TY - GEN

T1 - A Kleene analysis of Mobile Ambients

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

AU - Sagiv, M.

PY - 2000

Y1 - 2000

N2 - 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.

AB - 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.

M3 - Article in proceedings

SP - 305

EP - 319

BT - Proc. ESOP'00

PB - Springer Verlag

T2 - Proc. ESOP'00

Y2 - 1 January 2000

ER -

A Kleene analysis of Mobile Ambients

Abstract

Conference

OpenUrl availability

Fingerprint

Cite this