Abstract interpretation of mobile ambients

We show how abstract interpretation can be expressed in a constraint-based formalism that is becoming increasingly popular for the analysis of functional and object-oriented languages. This is illustrated by developing analyses for the ambient calculus. The first step of the development constructs an analysis for counting occurrences of processes inside other processes; we show that the analysis is semantically correct and that the set of acceptable solutions constitutes a Moore family. The second step considers a previously developed control flow analysis and shows how to induce it from the counting analysis; we show that its properties can be derived from those of the counting analysis using general results about abstract interpretation for constraint-based analyses.