Sciweavers

Share
FORTE
2009

Approximated Context-Sensitive Analysis for Parameterized Verification

8 years 1 months ago
Approximated Context-Sensitive Analysis for Parameterized Verification
Abstract. We propose a verification method for parameterized systems with global conditions. The method is based on context-sensitive constraints, a symbolic representation of infinite sets of configurations defined on top of words over a finite alphabet. We first define contextsensitive constraints for an exact symbolic backward analysis of parameterized systems with global conditions. Since the model is Turing complete, such an analysis is not guaranteed to terminate. To turn the method into a verification algorithm, we introduce context-sensitive constraints that over-approximate the set of backward reachable states and show how to symbolically test entailment and compute predecessors. We apply the resulting algorithm to automatically verify parameterized models for which the exact analysis and other existing verification methods either diverge or return false positives.
Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezin
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Where FORTE
Authors Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine
Comments (0)
books