Name
Abstract | ||
|---|---|---|
This paper gives an overview of the features offered by the tool 驴SPIN in order to perform abstract model checking of LTL formulas. Shortly, these features are: construction of over-approximated PROMELA models, checking satisfaction of universal formulas, checking refutation of existential formulas, and on-the-fly refinement of the model by means of a refinement of the temporal formula to be verified. |
Year | Venue | Keywords |
|---|---|---|
2003 | ACSD | Abstract Model Checking,existential formula,temporal formula,Temporal Logic,universal formula,LTL formula,over-approximated PROMELA model,abstract model checking,on-the-fly refinement |
DocType | ISBN | Citations |
Conference | 0-7695-1887-7 | 0 |
PageRank | References | Authors |
0.34 | 6 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| María del Mar Gallardo | 1 | 141 | 13.16 |
| Jesús Martínez | 2 | 51 | 5.72 |
| Pedro Merino | 3 | 201 | 25.98 |
| Ernesto Pimentel | 4 | 162 | 34.49 |