Amb-s.a.: A Static Analyzer for Mobile Ambients1
Version 1.01

Jérôme Feret


Amb-s.a. is an academic tool for statically inferring a sound description of the potential behaviour of a mobile system described in the Ambient-calculus. It uses Abstract Interpretation to infer both the control flow and occurrence number properties: Control flow analysis captures all the potential interactions between agents, it is precise enough to distinguish between recursive instances of the same agent. Occurrence number analysis captures both the number of agents that may be contained inside an ambient, and the number of agents that may occurs inside the whole system.

This document was translated from LATEX by HEVEA and HACHA.