Abstract interpretation based verification of temporal properties for BioAmbients

  • Gori R
  • Levi F
  • 3


    Mendeley users who have this article in their library.
  • 9


    Citations of this article.


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.

Author-supplied keywords

  • Abstract interpretation
  • Mobile Ambients and BioAmbients calculus
  • Verification of temporal properties

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Roberta Gori

  • Francesca Levi

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free