NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Swarm VerificationReportedly, supercomputer designer Seymour Cray once said that he would sooner use two strong oxen to plow a field than a thousand chickens. Although this is undoubtedly wise when it comes to plowing a field, it is not so clear for other types of tasks. Model checking problems are of the proverbial "search the needle in a haystack" type. Such problems can often be parallelized easily. Alas, none of the usual divide and conquer methods can be used to parallelize the working of a model checker. Given that it has become easier than ever to gain access to large numbers of computers to perform even routine tasks it is becoming more and more attractive to find alternate ways to use these resources to speed up model checking tasks. This paper describes one such method, called swarm verification.


Document ID
20150014777
Document Type
Conference Paper
External Source(s)
Authors
Holzmann, Gerard J. (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Joshi, Rajeev (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Groce, Alex (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Date Acquired
August 3, 2015
Publication Date
September 15, 2008
Subject Category
Computer Programming and Software
Meeting Information
IEEE/ACM International Conference on Automated Software Engineering(L''Aquila)
Distribution Limits
Public
Copyright
Other
Keywords
grid computing
logic model checking