JPF is the most popular model checking tool for Java applications. It is extensible and there are lots of extensions for various purposes. Jpf­nhandler is one of such extensions. Its goal is delegating the execution of SUT methods from JPF to JVM level. One goal of this project is to improve jpf-­nhandler performance using the cache layer. The latter prevents invoking methods more than once and problems caused by this. It also considerably increases the jpf­nhnandler efficiency as each method is executed only once. If jpf­nhandler encounters delegated method that has been executed, it just reflects result of its invocation. Another goal is to extend the converter component and including convertor classes for missing incompatible model classes.





  • franck
  • Nastaran
  • Cyrille Artho