This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Swarm Verification Techniques
November/December 2011 (vol. 37 no. 6)
pp. 845-857
ASCII Text
x 
 
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.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2010.110,
author = {Gerard J. Holzmann and Rajeev Joshi and Alex Groce},
title = {Swarm Verification Techniques},
journal ={IEEE Transactions on Software Engineering},
volume = {37},
number = {6},
issn = {0098-5589},
year = {2011},
pages = {845-857},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.110},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Swarm Verification Techniques
IS - 6
SN - 0098-5589
SP845
EP857
EPD - 845-857
A1 - Gerard J. Holzmann,
A1 - Rajeev Joshi,
A1 - Alex Groce,
PY - 2011
KW - Software engineering tools and techniques
KW - logic model checking
KW - distributed algorithms
KW - software verification.
VL - 37
JA - IEEE Transactions on Software Engineering
ER -
 
Gerard J. Holzmann, California Institute of Technology, Pasadena
Rajeev Joshi, California Institute of Technology, Pasadena
Alex Groce, Oregon State University, Corvallis
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.

[1] D.L. Bird and C.U. Munoz, "Automatic Generation of Random Self-Checking Test Cases," IBM System J., vol. 22, no. 3, pp. 229-245, 1983.
[2] T. Ball and S.K. Rajamani, "Automatically Validating Temporal Safety Properties of Interfaces," Proc. Spin Workshop Model Checking Software, pp. 103-122, May 2001.
[3] M.B. Dwyer et al., "Parallel Randomized State-Space Search," Proc. Int'l Conf. Software Eng., pp. 3-12, 2007.
[4] G.E. Moore, "Cramming More Components onto Integrated Circuits," Electronics, vol. 38, no. 8, pp. 114-117, Apr. 1965.
[5] G.J. Holzmann, "Tracing Protocols," AT&T Technical J., vol. 64, no. 10, pp. 2413-2433, Dec. 1985.
[6] G.J. Holzmann, "On Limits and Possibilities of Automated Protocol Analysis," Proc. Sixth Int'l Conf. Protocol Specification, Testing, and Verification, June 1987.
[7] G.J. Holzmann, "Logic Verification of ANSI-C Code with Spin," Proc. Seventh Spin Workshop, pp. 131-147, Aug. 2000.
[8] G.J. Holzmann, The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2004.
[9] G.J. Holzmann and M.H. Smith, "Automating Software Feature Verification," Bell Labs Technical J., vol. 5, no. 2, pp. 72-87, Apr.-June 2000.
[10] G.J. Holzmann and R. Joshi, "Model-Driven Software Verification," Proc. 11th Spin Workshop, pp. 77-92, Apr. 2004.
[11] G.J. Holzmann and D. Bosnacki, "The Design of a Multi-Core Extension to the Spin Model Checker," IEEE Trans. Software Eng., vol. 33, no. 10, pp. 659-674, Oct. 2007.
[12] G.J. Holzmann and M. Florian, "Model Checking with Bounded Context Switching," technical report, JPL LaRS Oct. 2009.
[13] A.E.J. Hyvärinen, T. Junttila, and I. Niemelä, "Strategies for Solving SAT in Grids by Randomized Search," Intelligent Computer Math., pp. 125-140, Springer, 2008.
[14] M. Musuvathi and S. Qadeer, "Fair Stateless Model Checking," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 7-13, June 2008.
[15] K. Ohmura and K. Ueda, "C-Sat: A Parallel SAT Solver for Clusters," Proc. 12th Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 524-537, 2009.
[16] D. Owen and T. Menzies, "Lurch: A Lightweight Alternative to Model Checking," Proc. 15th Int'l Conf. Software Eng. and Knowledge Eng., July 2003.
[17] J. Penix, W. Visser, C. Pasareanu, E. Engstrom, A. Larson, and N. Weininger, "Verifying Time Partitioning in the DEOS Scheduling Kernel," Formal Methods in Systems Design J., vol. 26, no. 2, Mar. 2005.
[18] C. West, "Protocol Validation in Complex Systems," Proc. Symp. Comm. Architecture and Protocols, pp. 303-312, 1989.
[19] S. Qadeer and J. Rehof, "Context-Bounded Model Checking," Proc. Tools and Algorithms for the Construction and Analysis of Systems, pp. 93-107, 2005.
[20] H. Sivaraj and G. Gopalakrishnan, "Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking," Proc. Second Int'l Workshop Parallel and Distributed Model Checking, July 2003.
[21] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, "Model Checking," Programs Int'l J. Automated Software Eng. vol. 10, no. 2, pp. 3-12, Apr. 2003.
[22] C.M. Wintersteiger, Y. Hamadi, and L.de Moura, "A Concurrent Portfolio Approach to SMT Solving," Proc. Int'l Conf. Computer Aided Verification, pp. 715-720, 2009.

Index Terms:
Software engineering tools and techniques, logic model checking, distributed algorithms, software verification.
Citation:
Gerard J. Holzmann, Rajeev Joshi, Alex Groce, "Swarm Verification Techniques," IEEE Transactions on Software Engineering, vol. 37, no. 6, pp. 845-857, Nov.-Dec. 2011, doi:10.1109/TSE.2010.110
Usage of this product signifies your acceptance of the Terms of Use.