Approximated context-sensitive analysis for parameterized verification

6Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.

This article is free to access.

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 context-sensitive 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. © 2009 Springer Berlin Heidelberg.

Cite

CITATION STYLE

APA

Abdulla, P. A., Delzanno, G., & Rezine, A. (2009). Approximated context-sensitive analysis for parameterized verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5522 LNCS, pp. 41–56). https://doi.org/10.1007/978-3-642-02138-1_3

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