Contributions
Students working with Darko Marinov have made several contributions to Java PathFinder (JPF), an explicit-state model checker for Java programs developed at NASA (and the first open-source project from NASA). These contributions add new functionality to JPF, improve its performance, or patch bugs. These contributions include the following:- Delayed Choice , which postpones non-deterministic choice of values until they are used, reducing the size of search tree. (submitted by Milos Gligoric and Tihomir Gvero)
- Undo Backtracking, which can speed up state-space exploration, specifically backtracking (submitted by Tihomir Gvero)
- Untracked Fields/Objects, which allows the user to mark that certain parts of the state should not be restored during backtracking (submitted by Milos Gligoric and Tihomir Gvero)
- Overflow checking, which can check for overflow in numeric instructions (submitted by Aleksandar Milicevic and Sasa Misailovic)
- Support for searches that bound the number of preemptive context switches during state-space exploration of multithreaded programs (submitted by Igor Andjelkovic, Steven Lauterburg and Mirko Stojmenovic)
- Eight bug patches submitted by Tihomir Gvero (array element type compatibility, arraycopy method type compatibility, annotation element types, casting primitive type arrays, output stream method, enumeration method, reflection method, cloning of primitive type arrays)
- Three bug patches submitted by Milos Gligoric (avoiding ChoiceGenerator creation, StackFrame resize, array store)
- One patch submitted by Mirko Stojmenovic, Igor Andjelkovic and Milos Gligoric (additional peer methods for java.lang.reflect classes)
last updated 02/14/2010