Advertisement

A Kleene Analysis of Mobile Ambients

  • Flemming Nielson
  • Hanne Riis Nielson
  • Mooly Sagiv
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)

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.

Keywords

Operational Semantic Predicate Symbol Capability Action Unary Predicate Replication Operation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    L. Cardelli, A. D. Gordon: Mobile ambients. In Proc. FoSSaCS’98, vol. 1378 of LNCS, pages 140–155, Springer, 1998.Google Scholar
  2. 2.
    L. Cardelli, A. D. Gordon: Types for mobile ambients. In Proc. POPL’99, ACM Press, 1999.Google Scholar
  3. 3.
    L. Cardelli, G. Ghelli, A. D. Gordon: Mobility types for mobile ambients. In Proc. ICALP’99, LNCS, Springer, 1999.Google Scholar
  4. 4.
    L. Cardelli and A. D. Gordon: Anytime, Anywhere: Modal Logics for Mobile Ambients. In Proc. POPL’00, ACM Press, 2000.Google Scholar
  5. 5.
    D.R. Chase, M. Wegman, and F. Zadeck. Analysis of pointers and structures. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 296–310, ACM Press, 1990.Google Scholar
  6. 6.
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Symp. on Princ. of Prog. Lang., pages 269–282, ACM Press, 1979.Google Scholar
  7. 7.
    R.L. Epstein. The Semantic Foundations of Logic, Volume 1: Propositional Logics. Kluwer Academic Publishers, 1990.Google Scholar
  8. 8.
    M.L. Ginsberg. Multivalued logics: A uniform approach to inference in artificial intelligence. In Comp. Intell., 4:265–316, 1988.CrossRefGoogle Scholar
  9. 9.
    R. R. Hansen, J. G. Jensen, F. Nielson, H. Riis Nielson: Abstract Interpretation of Mobile Ambients. In Proc. SAS’99, vol. 1694 of LNCS, Springer, 1999.Google Scholar
  10. 10.
    H. Hoddes. Three-Valued Logics: An Introduction, A Comparison of Various Logical Lexica, and Some Philosophical Remarks. In Annals of Pure and Applied Logic, 1989.Google Scholar
  11. 11.
    S.C. Kleene. Introduction to Metamathematics. North-Holland, second edition, 1987.Google Scholar
  12. 12.
    T. Lev-Ami: TVLA: a framework for Kleene based static analysis. M.Sc. thesis, Tel Aviv University, January 2000.Google Scholar
  13. 13.
    F. Levi and D. Sangiorgi: Controlling Interference in Ambients. In Proc. POPL’00, ACM Press, 2000.Google Scholar
  14. 14.
    F. Nielson: Semantics-Directed Program Analysis: A Tool-Maker’s Perspective. In Proc. SAS’96, vol. 1145 of LNCS, Springer, 1996.Google Scholar
  15. 15.
    F. Nielson, H. Riis Nielson, C. L. Hankin: Principles of Program Analysis, Springer, 1999.Google Scholar
  16. 16.
    F. Nielson, H. Riis Nielson, R. R. Hansen, J. G. Jensen: Validating Firewalls in Mobile Ambients. In Proc. CONCUR’99, vol. 1664 of LNCS, Springer, 1999.Google Scholar
  17. 17.
    F. Nielson, H. Riis Nielson: Shape Analysis for Mobile Ambients. In Proc. POPL’00, ACM Press, 2000.Google Scholar
  18. 18.
    M. Sagiv, T. Reps, R. Wilhelm: Parametric Shape Analysis via 3-Valued Logic. In Proc. POPL’99, ACM Press, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Flemming Nielson
    • 1
  • Hanne Riis Nielson
    • 1
  • Mooly Sagiv
    • 2
  1. 1.Aarhus UniversityAarhus
  2. 2.Tel Aviv UniversityTel Aviv

Personalised recommendations