Abstract interpretation based verification of temporal properties for BioAmbients

Citations of this article
Mendeley users who have this article in their library.
Get full text


This paper concerns the application of formalmethods to biological systems, modeledspecifically in BioAmbients, a variant of the Mobile Ambients calculus. Following the semanticbased approach of abstract interpretation, we define a new static analysis that computes an abstract transition system. Our analysis has two main advantages with respect to the analyses appearing in the literature: (i) it is able to address temporal properties which are more general than invariant properties; (ii) it supports, by means of a particular labeling discipline, the validation of systems where several copies of an ambient may appear. We also design new weaker and more efficient analyses by means of simple widening operators. © 2010 Elsevier Inc. All rights reserved.




Gori, R., & Levi, F. (2010). Abstract interpretation based verification of temporal properties for BioAmbients. Information and Computation, 208(8), 869–921. https://doi.org/10.1016/j.ic.2010.03.004

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free