Name
Abstract | ||
|---|---|---|
Verification of multi-threaded C++ programs poses three major challenges: the large number of states, states with huge sizes, and time intensive expansions of states. This paper presents our efforts in addressing these issues by combining an efficient use of hard disk with the distribution of the state space on several computing nodes. The approach is applicable to clusters and multi-core machines with single or multiple hard disks. We exploit the concept of a signature of a state that allows the full state vector to stay on secondary memory. For a distributed exploration of the state space, we report the lessons learned from using different partitioning schemes, including Holzmann and Bosnacki's [G. Holzmann and D. Bosnacki. The design of a multi-core extension of the Spin Model Checker. IEEE Trans. on Software Engineering, 2007. To Appear] depth-slicing method, and their effects on blind and directed search algorithms. Empirical evaluation is done on our experimental C++ verification tool StEAM, which is capable of detecting errors such as segmentation faults, deadlocks, access conflicts, etc. The distributed algorithms are realized through MPI on a cluster of workstations. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1016/j.entcs.2007.10.019 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
multi-core machine,multi-core extension,hard disk,which is capable of detecting errors such as segmentation faults,access conflicts,full state vector,deadlocks,multiple hard disk,distributed model checking,multi-threaded c,external model checking,etc. the distributed algorithms are realized through mpi on a cluster of workstations. key words: program verification,experimental c,external model checking.,verification tool steam,program verification,empirical evaluation is done on our experimental c++ verification tool steam,state space,g. holzmann,model checking,distributed algorithm | State vector,Search algorithm,Computer science,Deadlock,Workstation,Theoretical computer science,Distributed algorithm,State space,Auxiliary memory,SPIN model checker,Distributed computing | Journal |
Volume | Issue | ISSN |
198 | 1 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
1 | 0.35 | 30 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stefan Edelkamp | 1 | 1557 | 125.46 |
| Shahid Jabbar | 2 | 138 | 9.03 |
| Damian Sulewski | 3 | 87 | 6.45 |