Abstract
| Original language | Undefined |
|---|---|
| Title of host publication | Proceedings of the 10th International Haifa Verification Conference, HVC 2014 |
| Place of Publication | Berlin |
| Publisher | Springer |
| Pages | 204-219 |
| Number of pages | 16 |
| ISBN (Print) | 978-3-319-13337-9 |
| DOIs | |
| Publication status | Published - Nov 2014 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Verlag |
| Volume | 8855 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Keywords
- EWI-25296
- METIS-309656
- IR-93290
Cite this
}
Read, Write and Copy Dependencies for Symbolic Model Checking. / Meijer, Jeroen; Kant, Gijs; Blom, Stefan; van de Pol, Jan Cornelis.
Proceedings of the 10th International Haifa Verification Conference, HVC 2014. Berlin : Springer, 2014. p. 204-219 (Lecture Notes in Computer Science; Vol. 8855).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - Read, Write and Copy Dependencies for Symbolic Model Checking
AU - Meijer, Jeroen
AU - Kant, Gijs
AU - Blom, Stefan
AU - van de Pol, Jan Cornelis
N1 - 10.1007/978-3-319-13338-6_16
PY - 2014/11
Y1 - 2014/11
N2 - This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values. We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.
AB - This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values. We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.
KW - EWI-25296
KW - METIS-309656
KW - IR-93290
U2 - 10.1007/978-3-319-13338-6_16
DO - 10.1007/978-3-319-13338-6_16
M3 - Conference contribution
SN - 978-3-319-13337-9
T3 - Lecture Notes in Computer Science
SP - 204
EP - 219
BT - Proceedings of the 10th International Haifa Verification Conference, HVC 2014
PB - Springer
CY - Berlin
ER -