Configuring Java Pathfinder for concurrent Java programs

Sammanfattning: Software verification is a field of computer science dedicated to guar- antee that a program runs according to a formalized specification. Of various kinds of verification techniques model checking tries all possi- ble states of a program and makes sure each state satisfies a set of for- malized properties. Java Pathfinder (JPF) is a tool that automatically model checks Java bytecode. This report studies general configuration patterns for JPF that leads it to either terminate without errors or ter- minate with found concurrency bugs for different types of programs. The types considered are solutions to producer-consumer problems, barber shop problems, reader-writer problems and programs falling under the type server-client systems. The main part of the method is first a search for these types of programs using cloud-based revision control systems. Second, these programs are verified with the help of the JPF documentation, articles on the subject and online discus- sion groups. The results are configurations that lead to no errors, con- currency bugs and native method errors depending on the program verified. An important limitation of the report is the absence of large programs that challenge JPF’s state space handling. The resulting gen- eral configuration patterns found are applicable to small programs not using native methods. A pattern is also found for programs with na- tive methods, but here it is possible that the user must modify a model class in JPF.