AbstractThe ambient calculus is a calculus of computation that allows active processes to move between sites. We present an analysis inspired by state-of-the-art pointer analyses that safely and accurately predicts which processes may turn up at what sites during the execution of a composite system. The analysis models sets of processes by sets of regular tree grammars enhanced with context dependent counts, and it obtains its precision by combining a powerful redex materialisation with a strong redex reduction (in the manner of the strong updates performed in pointer analyses).
Categories and Subject Descriptors: D.3 [Programming Languages]; F.3 [Logics and Meanings of Programs]; F.4 [Mathematical Logic and Formal Languages]
Additional Key Words and Phrases: mobile ambients, static analysis, shape analysis
Selected references
- Prateek Mishra and Uday S. Reddy. Declaration-free type checking. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 7-21, New Orleans, Louisiana, January 1985.