Publication at Faculty of Mathematics and Physics |
2010
Abstract
Software model checkers are being used mostly to discover specific types of errors in the code, since exhaustive verification of complex programs is not possible due to state explosion. Moreover, typical model checkers cannot be directly applied to isolated components such as libraries or individual classes.
A common solution is to create an abstract environment for a component to be checked. In this paper we present a method that allows to discover at least some concurrency errors in component's code in reasonable time.
The key ideas of our method are (i) use of an abstract environment that performs a random sequence of method calls in each thread, and (ii) restarts of the error detection process according to a specific strategy.