
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Gerard J. Holzmann, Dragan Bosnacki, "The Design of a Multicore Extension of the SPIN Model Checker," IEEE Transactions on Software Engineering, vol. 33, no. 10, pp. 659674, October, 2007.  
BibTex  x  
@article{ 10.1109/TSE.2007.70724, author = {Gerard J. Holzmann and Dragan Bosnacki}, title = {The Design of a Multicore Extension of the SPIN Model Checker}, journal ={IEEE Transactions on Software Engineering}, volume = {33}, number = {10}, issn = {00985589}, year = {2007}, pages = {659674}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2007.70724}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  The Design of a Multicore Extension of the SPIN Model Checker IS  10 SN  00985589 SP659 EP674 EPD  659674 A1  Gerard J. Holzmann, A1  Dragan Bosnacki, PY  2007 KW  Software/Program Verification KW  Model Checking KW  Models of Computation KW  Logics and meanings of Programs KW  Distributed Programming VL  33 JA  IEEE Transactions on Software Engineering ER   
[1] R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani, “PartialOrder Reduction in Symbolic StateSpace Exploration,” Formal Methods in System Design, vol. 18, pp. 97116, 2001.
[2] J. Barnat, L. Brim, and J. Stribrna, “Distributed LTL ModelChecking in SPIN,” Proc. Eighth Int'l SPIN Workshop Model Checking of Software, May 2001.
[3] J. Barnat, L. Brim, and J. Chaloupka, “Parallel BreadthFirst Search LTL Model Checking,” Proc. Automated Software Eng., 2003.
[4] G. Behrmann, T. Hune, and F. Vaandrager, “Distributing Timed Model Checking—How the Search Order Matters,” Proc. 12th Int'l Conf. Computer Aided Verification, pp. 216231, 2000.
[5] D. Bosnacki and G.J. Holzmann, “Improving SPIN's PartialOrder Reduction for BreadthFirst Search,” Proc. 12th Int'l SPIN Workshop, pp. 91105, 2005.
[6] L. Brim, I. Cerna, P. Moravec, and J. Simsa, “Accepting Predecessors Are Better than Back Edges in Distributed LTL Model Checking,” Formal Methods in Computer Aided Design, pp.266352, 2004.
[7] L. Brim, I. Cerna, P. Moravec, and J. Simsa, “Distributed Partial Order Reduction of State Spaces,” Electronic Notes in Theoretical Computer Science, vol. 128, pp. 6374, 2005.
[8] L. Brim, I. Cerna, P. Moravec, and J. Simsa, “How to Order Vertices for Distributed LTL ModelChecking Based on Accepting Predecessors,” Electronic Notes in Theoretical Computer Science, vol. 135, pp. 318, 2006.
[9] I. Cerna and R. Pelanek, “Distributed Explicit Fair Cycle Detection,” Proc. SPIN Workshop, pp. 4973, 2003.
[10] S. Chien et al., “Using Autonomy Flight Software to Improve Science Return on Earth Observing One (EO1),” J. Aerospace Computing, Information, and Comm., Apr. 2005.
[11] E.W. Dijkstra, “Shmuel Safra's Version of Termination Detection,” EWD998, Jan. 1987.
[12] S. Edelkamp and S. Jabar, “LargeScale Directed Model Checking LTL,” Proc. 13th Int'l SPIN Workshop, pp. 118, 2006.
[13] P.R. Gluck and G.J. Holzmann, “Using Spin Model Checking for Flight Software Verification,” Proc. 2002 Aerospace Conf., Mar. 2002.
[14] P. Godefroid, Partial Order Methods for the Verification of Concurrent Systems: An Approach to the State Space Explosion. Springer Verlag, 1996.
[15] G.J. Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1991.
[16] G.J. Holzmann, P. Godefroid, and D. Pirottin, “Coverage Preserving Reduction Strategies for Reachability Analysis,” Proc. 12th Int'l Conf. Protocol Specification Testing and Verification, pp. 349363, June 1992.
[17] G.J. Holzmann and D. Peled, “An Improvement in Formal Verification,” Proc. Conf. Formal Description Techniques, Oct. 1994.
[18] G.J. Holzmann, D. Peled, and M. Yannakakis, “On Nested DepthFirst Search,” The SPIN Verification System, pp. 2332, Am. Math. Soc., 1996.
[19] G.J. Holzmann and M.H. Smith, “Automating Software Feature Verification,” Bell Labs Technical J., vol. 5, no. 2, pp. 7287, Apr.June 2000.
[20] G.J. Holzmann, The SPIN Model Checker—Primer and Reference Manual. AddisonWesley, 2004.
[21] G.J. Holzmann and R. Joshi, “ModelDriven Software Verification,” Proc. 11th SPIN Workshop, pp. 7792, Apr. 2004.
[22] G.J. Holzmann, “A StackSlicing Algorithm for MultiCore Model Checking,” Proc. Sixth Int'l Workshop Parallel and Distributed Methods on Verification, July 2007.
[23] C.P. Inggs and H. Barringer, “Effective State Exploration for Model Checking on a Shared Memory Architecture,” Electronic Notes in Theoretical Computer Science, vol. 68, no. 4, 2002.
[24] C.P. Inggs and H. Barringer, “${\rm CTL}^{\ast}$ Model Checking on a SharedMemory Architecture,” Electronic Notes in Theoretical Computer Science, vol. 128, pp. 107123, 2005.
[25] S. Jabbar and S. Edelkamp, “Parallel External Directed Model Checker with Linear I/O,” Proc. Seventh Int'l Conf. Verification, Model Checking, and Abstract Interpretation, pp. 237251, 2006.
[26] R. Joshi and G.J. Holzmann, “A MiniChallenge: Build a Verifiable Filesystem,” Formal Aspects of Computing, vol. 19, 2007.
[27] R. Kumar and E.G. Mercer, “Load Balancing Parallel Explicit State Model Checking,” Proc. Third Int'l Workshop Parallel and Distributed Model Checking, Aug. 2004.
[28] R.P. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün, “Static Partial Order Reduction,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98), pp. 345357, 1998.
[29] A.L. Lafuente, “Simplified Distributed LTL Model Checking by Localizing Cycles,” Technical Report 00176, Institut fur Informatik, Univ. Freiburg, Germany, July 2002.
[30] F. Lerda and R. Sisto, “DistributedMemory Model Checking in SPIN,” Proc. SPIN Workshop, 1999.
[31] G.E. Moore, “Cramming More Components onto Integrated Circuits,” Electronics, vol. 38, pp. 114117, 1965.
[32] D. Peled, “Combining Partial Order Reductions with OntheFly ModelChecking,” Proc. Conf. Computer Aided Verification (CAV '94), pp. 377390, 1994.
[33] 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.
[34] G.L. Peterson, “Myths about the Mutual Exclusion Problem,” Information Processing Letters, vol. 12, no. 3, pp. 115116, June 1981.
[35] R. Pelanek, “Typical Properties of State Spaces,” Proc. 11th SPIN Workshop, pp. 522, Apr. 2004.
[36] J.H. Reif, “Depth First Search Is Inherently Sequential,” Information Processing Letters, vol. 20, no. 5, pp. 229234, June 1985.
[37] U. Stern and D. Dill, “Parallelizing the Mur$\varphi$ Verifier,” Proc. Ninth Int'l Conf. Computer Aided Verification, pp. 256278, June 1997.
[38] A. Valmari, “The State Explosion Problem,” Lectures on Petri Nets I: Basic Models, Springer, pp. 429528, 1998.