Hybrid Logical Analyses of the Ambient Calculus

Thomas Bolander, René Rydhof Hansen

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    In this paper, hybrid logic is used to formulate a rational reconstruction of a previously published control flow analysis for the mobile ambients calculus and we further show how a more precise flow-sensitive analysis, that takes the ordering of action sequences into account, can be formulated in a natural way. We show that hybrid logic is very well suited to express the semantic structure of the ambient calculus and how features of hybrid logic can be exploited to reduce the "administrative overhead" of the analysis specification and thus simplify it. Finally, we use HyLoTab, a fully automated theorem prover for hybrid logic, both as a convenient platform for a prototype implementation as well as to formally prove the correctness of the analysis.
    Original languageEnglish
    Title of host publicationLogic, Language, Information and Computation, Proceedings
    PublisherSpringer
    Publication date2007
    Pages83-100
    ISBN (Print)978-3-540-73443-7
    DOIs
    Publication statusPublished - 2007
    Event14th Workshop on Logic, Language, Information and Computation (WoLLIC) - Rio de Janeiro, Brazil
    Duration: 2 Jul 20075 Jul 2007
    Conference number: 14

    Conference

    Conference14th Workshop on Logic, Language, Information and Computation (WoLLIC)
    Number14
    CountryBrazil
    CityRio de Janeiro
    Period02/07/200705/07/2007
    SeriesLecture Notes in Computer Science
    Volume4576
    ISSN0302-9743

    Keywords

    • hybrid logic
    • static analysis
    • mobile ambients

    Fingerprint Dive into the research topics of 'Hybrid Logical Analyses of the Ambient Calculus'. Together they form a unique fingerprint.

    Cite this