Context-bounded model checking of concurrent software
In: TACAS 2005 : tools and algorithms for the construction and analysis of systems (Edinburgh, 4-8 April 2005)Lecture notes in computer science :93-107
Konferenz
- print, 30 ref
Zugriff:
The interaction among concurrently executing threads of a program results in insidious programming errors that are difficult to reproduce and fix. Unfortunately, the problem of verifying a concurrent boolean program is undecidable [24]. In this paper, we prove that the problem is decidable, even in the presence of unbounded parallelism, if the analysis is restricted to executions in which the number of context switches is bounded by an arbitrary constant. Restricting the analysis to executions with a bounded number of context switches is unsound. However, the analysis can still discover intricate bugs and is sound up to the bound since within each context, a thread is fully explored for unbounded stack depth. We present an analysis of a real concurrent system by the ZING model checker which demonstrates that the ability to model check with arbitrary but fixed context bound in the presence of unbounded parallelism is valuable in practice. Implementing context-bounded model checking in ZING is left for future work.
Titel: |
Context-bounded model checking of concurrent software
|
---|---|
Autor/in / Beteiligte Person: | QADEER, Shaz ; REHOF, Jakob |
Link: | |
Quelle: | TACAS 2005 : tools and algorithms for the construction and analysis of systems (Edinburgh, 4-8 April 2005)Lecture notes in computer science :93-107 |
Veröffentlichung: | Berlin: Springer, 2005 |
Medientyp: | Konferenz |
Umfang: | print, 30 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|