Hybrid Logical Analyses of the Ambient Calculus

Thomas Bolander, René Rydhof Hansen

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


    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
    Publication date2007
    ISBN (Print)978-3-540-73443-7
    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


    Conference14th Workshop on Logic, Language, Information and Computation (WoLLIC)
    CityRio de Janeiro
    SeriesLecture Notes in Computer Science


    • 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