TY - GEN
T1 - Tackling large verification problems with the swarm tool
AU - Holzmann, Gerard J.
AU - Joshi, Rajeev
AU - Groce, Alex
N1 - Funding Information:
The research described in this paper was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration. The work was supported in part by NASA’s Exploration Technology Development Program (ETDP) on Reliable Software Engineering.
PY - 2008
Y1 - 2008
N2 - The range of verification problems that can be solved with logic model checking tools has increased significantly in the last few decades. This increase in capability is based on algorithmic advances, but in no small measure it is also made possible by increases in processing speed and main memory sizes on standard desktop systems. For the time being, though, the increase in CPU speeds has mostly ended as chip-makers are redirecting their efforts to the development of multi-core systems. In the coming years we can expect systems with very large memory sizes, and increasing numbers of CPU cores, but with each core running at a relatively low speed. We will discuss the implications of this important trend, and describe how we can leverage these developments with new tools.
AB - The range of verification problems that can be solved with logic model checking tools has increased significantly in the last few decades. This increase in capability is based on algorithmic advances, but in no small measure it is also made possible by increases in processing speed and main memory sizes on standard desktop systems. For the time being, though, the increase in CPU speeds has mostly ended as chip-makers are redirecting their efforts to the development of multi-core systems. In the coming years we can expect systems with very large memory sizes, and increasing numbers of CPU cores, but with each core running at a relatively low speed. We will discuss the implications of this important trend, and describe how we can leverage these developments with new tools.
UR - http://www.scopus.com/inward/record.url?scp=54249169176&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=54249169176&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-85114-1_11
DO - 10.1007/978-3-540-85114-1_11
M3 - Conference contribution
AN - SCOPUS:54249169176
SN - 3540851135
SN - 9783540851134
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 134
EP - 143
BT - Model Checking Software - 15th International SPIN Workshop, Proceedings
T2 - 15th International SPIN Workshop on Model Checking of Software, SPIN 2008
Y2 - 10 August 2008 through 12 August 2008
ER -