Bounded Model Checking Using Java PathFinder

This thesis deals with the application of bounded model checking method for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing