Abstract
| Language | Undefined |
|---|---|
| Title of host publication | Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 |
| Editors | S. Ramesh |
| Place of Publication | London |
| Publisher | Springer Verlag |
| Pages | 269-283 |
| Number of pages | 15 |
| ISBN (Print) | 978-3-642-33386-6 |
| DOIs | |
| State | Published - 3 Oct 2012 |
| Event | 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 - Thiruvananthapuram, India Duration: 3 Oct 2012 → 6 Oct 2012 Conference number: 10 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Verlag |
| Volume | 7561 |
Conference
| Conference | 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 |
|---|---|
| Abbreviated title | ATVA |
| Country | India |
| City | Thiruvananthapuram |
| Period | 3/10/12 → 6/10/12 |
Keywords
- METIS-287890
- CNDFS
- IR-80818
- LTL model checking
- LTSMIN
- Verification
- EWI-21967
- Multi-Core
- liveness properties
- paralll
- nested depth-first search
- FMT-MC: MODEL CHECKING
- NDFS
Cite this
}
Improved Multi-Core Nested Depth-First Search. / Evangelista, Sami; Laarman, Alfons; Petrucci, Laure; van de Pol, Jan Cornelis.
Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012. ed. / S. Ramesh. London : Springer Verlag, 2012. p. 269-283 (Lecture Notes in Computer Science; Vol. 7561).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
TY - GEN
T1 - Improved Multi-Core Nested Depth-First Search
AU - Evangelista,Sami
AU - Laarman,Alfons
AU - Petrucci,Laure
AU - van de Pol,Jan Cornelis
PY - 2012/10/3
Y1 - 2012/10/3
N2 - This paper presents CNDFS, a tight integration of two earlier multi-core nested depth-first search (NDFS) algorithms for LTL model checking. CNDFS combines the different strengths and avoids some weaknesses of its predecessors. We compare CNDFS to an earlier ad-hoc combination of those two algorithms and show several benefits: It has shorter and simpler code and a simpler correctness proof. It exhibits more stable performance and scalability, while at the same time reducing memory requirements. The algorithm has been implemented in the multi-core backend of the LTSmin model checker, which is now benchmarked for the first time on a 48 core machine (previously 16). The experiments demonstrate better scalability than other parallel LTL model checking algorithms, but we also investigate apparent bottlenecks. Finally, we noticed that the multi-core NDFS algorithms produce shorter counterexamples, surprisingly often shorter than their BFS-based counterparts.
AB - This paper presents CNDFS, a tight integration of two earlier multi-core nested depth-first search (NDFS) algorithms for LTL model checking. CNDFS combines the different strengths and avoids some weaknesses of its predecessors. We compare CNDFS to an earlier ad-hoc combination of those two algorithms and show several benefits: It has shorter and simpler code and a simpler correctness proof. It exhibits more stable performance and scalability, while at the same time reducing memory requirements. The algorithm has been implemented in the multi-core backend of the LTSmin model checker, which is now benchmarked for the first time on a 48 core machine (previously 16). The experiments demonstrate better scalability than other parallel LTL model checking algorithms, but we also investigate apparent bottlenecks. Finally, we noticed that the multi-core NDFS algorithms produce shorter counterexamples, surprisingly often shorter than their BFS-based counterparts.
KW - METIS-287890
KW - CNDFS
KW - IR-80818
KW - LTL model checking
KW - LTSMIN
KW - Verification
KW - EWI-21967
KW - Multi-Core
KW - liveness properties
KW - paralll
KW - nested depth-first search
KW - FMT-MC: MODEL CHECKING
KW - NDFS
U2 - 10.1007/978-3-642-33386-6_22
DO - 10.1007/978-3-642-33386-6_22
M3 - Conference contribution
SN - 978-3-642-33386-6
T3 - Lecture Notes in Computer Science
SP - 269
EP - 283
BT - Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
PB - Springer Verlag
CY - London
ER -