Project Name


java.util.concurrent contains many classes including native methods. The jpf-concurrent project supports many of these classes by using model classes and native peer classes. A part of java.util.concurrent is java.util.concurrent.atomic which can be used to implement lock-free algorithms. This project includes providing support for unhandled native calls within java.util.concurrent. Moreover, regression tests will be performed to ensure the compatibility of this package with jpf-concurrent.


student: Nastaran Shafiei <nastaran.shafiei AT>

mentor: Mateusz Ujma <mateusz.ujma AT>



The sources for this project are located in the JPF extension called jpf-concurrent.


This project extended jpf-concurrent to support new classes from java.util.concurrent package. Specifically, eight new classes were implemented along with a test suite for each of them. More details are available in the paper "Mateusz Ujma and Nastaran Shafiei, jpf-concurrent: an extension of Java PathFinder for java.util.concurrent" which has been sucessfully submitted to "The Java Pathfinder Workshop 2011".

Last modified 6 years ago Last modified on 02/23/2012 02:55:22 PM