|
 
|
[EP07] Some Solutions to the Ignoring Problem
Conférence Internationale avec comité de lecture : SPIN'07 Int. Workshop on Model Checking Software, January 2007, Vol. 4595(14), pp.76-94, Series LNCS,
motcle:
Résumé:
The ignoring problem refers to the fact that some actions may be infinitely
postponed by a state space search algorithm that makes use of partial order
reduction (POR).
The prevention of this phenomenon is mandatory if one wants to verify more
elaborate properties than the deadlock freeness, e.g., safety or liveness
properties.
We present in this work some solutions to this problem.
In order to assess the quality of our propositions, we included them in our
model checker Helena.
We report the result of some experiments which show that our algorithms yield
better reductions than state of the art algorithms like those implemented in
the Spin tool.
BibTeX
| @inproceedings { | |||
| EP07, | |||
| title | = | "{Some Solutions to the Ignoring Problem}", | |
| author | = | " S. Evangelista and C. Pajault ", | |
| booktitle | = | "{SPIN'07 Int. Workshop on Model Checking Software}", | |
| year | = | 2007, | |
| month | = | "January", | |
| series | = | "LNCS", | |
| volume | = | 4595, | |
| issue | = | 14, | |
| pages | = | "76-94", | |
| } | |||
