Conference paper
Hybrid Logical Analyses of the Ambient Calculus
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2007 |
Pages: | 83-100 |
Proceedings: | 14th Workshop on Logic, Language, Information and Computation (WoLLIC)Workshop on Logic, Language, Information and Computation |
Series: | Lecture Notes in Computer Science |
ISBN: | 3540734430 , 3540734457 , 9783540734437 and 9783540734451 |
ISSN: | 03029743 |
Types: | Conference paper |
DOI: | 10.1007/978-3-540-73445-1_7 |
ORCIDs: | Bolander, Thomas |