Issue No.06 - November/December (2011 vol.37)
Gerard J. Holzmann , California Institute of Technology, Pasadena
Rajeev Joshi , California Institute of Technology, Pasadena
Alex Groce , Oregon State University, Corvallis
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.110
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 and new theoretical insights, but it has also benefitted from the steady increase in processing speeds and main memory sizes on standard computers. The steady increase in processing speeds, though, ended when chip-makers started redirecting their efforts to the development of multicore systems. For the near-term future, we can anticipate the appearance of systems with large numbers of CPU cores, but without matching increases in clock-speeds. We will describe a model checking strategy that can allow us to leverage this trend and that allows us to tackle significantly larger problem sizes than before.
Software engineering tools and techniques, logic model checking, distributed algorithms, software verification.
Gerard J. Holzmann, Rajeev Joshi, Alex Groce, "Swarm Verification Techniques", IEEE Transactions on Software Engineering, vol.37, no. 6, pp. 845-857, November/December 2011, doi:10.1109/TSE.2010.110