Abstract
We demonstrate that abstract interpretation is useful for analysing calculi of computation such as the ambient calculus (which is based on the π-calculus); more importantly, we show that the entire development can be expressed in a constraint-based formalism that is becoming exceedingly popular for the analysis of functional and object-oriented languages.
The first step of the development is an analysis for counting occurrences of processes inside other processes (for which we show semantic correctness and that solutions constitute a Moore family); the second step is a previously developed control ow analysis that we show how to induce from the counting analysis (and its properties are derived from those of the counting analysis using general results).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Control Flow Analysis for the π-calculus. In Proc. CONCUR’98, volume 1466 of Lecture Notes in Computer Science, pages 84–98. Springer-Verlag, 1998.
C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Static Analysis of Processes for No Read-Up and No Write-Down. In Proc. FoSSaCS’99, volume 1578 of Lecture Notes in Computer Science, pages 120–134. Springer-Verlag, 1999.
L. Cardelli and A. D. Gordon. Mobile Ambients. In Proc. FoSSaCS’98, volume 1378 of Lecture Notes in Computer Science, pages 140–155. Springer-Verlag, 1998.
L. Cardelli and A. D. Gordon. Types for Mobile Ambients. In Proc. POPL’99, pages 79–92. ACM Press, 1999.
R. R. Hansen and J. G. Jensen. Flow Logics for Mobile Ambients. M.Sc. thesis, Aarhus University, 1999.
T. Jensen, D. LeMétayer, and T. Thorn. Security and Dynamic Class Loading in Java: A Formalisation. Technical report, IRISA, Rennes, 1997.
F. Nielson, H. R. Nielson, R. R. Hansen, and J. G. Jensen. Validating Firewalls in Mobile Ambients. In Proc. CONCUR’99, Lecture Notes in Computer Science. Springer-Verlag, 1999. To appear.
A. Venet. Abstract Interpretation of the π-calculus. In Analysis and Verification of Multiple-Agent Languages, volume 1192 of Lecture Notes in Computer Science, pages 51–75. Springer-Verlag, 1997.
A. Venet. Automatic Determination of Communication Topologies in Mobile Systems. In Proc. SAS’98, volume 1503 of Lecture Notes in Computer Science, pages 152–167. Springer-Verlag, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rydhof Hansen, R., Jensen, J.G., Nielson, F., Nielson, H.R. (1999). Abstract Interpretation of Mobile Ambients. In: Cortesi, A., Filé, G. (eds) Static Analysis. SAS 1999. Lecture Notes in Computer Science, vol 1694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48294-6_9
Download citation
DOI: https://doi.org/10.1007/3-540-48294-6_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66459-8
Online ISBN: 978-3-540-48294-9
eBook Packages: Springer Book Archive