Journal article · Conference paper
Hybrid Logical Analyses of the Ambient Calculus
In
Information and Computation
—
2010, Volume 208, Issue 5, pp. 433-449
Abstract
In this paper, hybrid logic is used to formulate three control flow analyses for Mobile Ambients, a process calculus designed for modelling mobility. 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. (C) 2009 Elsevier Inc. All rights reserved.
| Language: | English |
|---|---|
| Year: | 2010 |
| Pages: | 433-449 |
| Proceedings: | 14th Workshop on Logic, Language, Information and Computation (WoLLIC)Workshop on Logic, Language, Information and Computation |
| ISSN: | 10902651 and 08905401 |
| Types: | Journal article and Conference paper |
| DOI: | 10.1016/j.ic.2009.01.006 |
| ORCIDs: | Bolander, Thomas |
Keywords
