.

Java PathFinder Summer of Code ProjectsMentors: John Penix, Peter Mehlitz, Corina Pasareanu, Dimitra Giannakopoulou, Darko Marinov, Tao Xie, Sarfraz Khurshid

.

http://javapathfinder.sourceforge.net/

.

For project questions contact javapathfinder-devel@lists.sourceforge.net

.

ProjectDifficultyLevel of interestMentorComments

.

Build a JPF extension for model checking distributed applications. This specifically involves modeling of the java.net package by means of JPF's "Model Java Interface" (MJI) mechanism.Medium1TBDFamiliarity with java.net or network programming would be helpful. There is work from Prof. Tevfik Bultan's group published in last year's Automated Software Engineering Conference that can be a starting point for this.

.

Build a suite of JPF conformance tests to test JVM compatability.Easy/Medium2TBD

.

Create a set of JPF text book examples. Collect example Java programs from text books - mostly multi-threaded examples - and add them to the JPF example sets. Document expected behavior and create buggy versions to demonstrate how JPF find errors.Easy14 (no more please)TBDSuggest one or two text books. Multiple people could work on this if working from different books.

.

Develop more state extensions for JPF (e.g., use re-execution rather
than storing/restoring full states or undoing/redoing writes.) This could especially include adaptive modes which choose an optimal mix between data and operation storage based on memory or execution speed goals
Medium/HardTBD

.

Develop models of java.util.concurrent implementation to allow more efficient model checking of programs that use these consructs. The underlying mechanisms for this package use undocumented, platform dependent classes that could be bypassed if the library modeling would take place at the level of public constructs like Semaphore etc. Medium3John PenixThis could be a great way to learn the details of java.util.concur

.

Create a JPF user interface in an IDE like Eclipse or NetBeans. JPF runs could be controlled by using JPF property files, the IDE would display both progress information and structured reports, using a customized JPF Publisher implementation Easy/Medium8TBDExperience with Eclipse helpful, but not required to get a good start on this.

.

Create a JPF version that can store and retrieve program states on/from a server, so that it is more easy to use JPF on huge state spaces. The model checker would run on a workstation, but would use a network interface to store and retrieve state data from an external server that does not even run Java (e.g. by using the Java serialization API)Medium/HardTBDThis would require some knowledge/experience with web server frameworks.

.

Create a visualization for JPF's statechart model checking extension. This would create UML state machine diagrams out of JPF state machine models, and animate traces of event sequences produced by the model checkerEasy/Medium1TBDThis would use the JPF listener API and be relatively stand-alone (and therefore easy to make fast progress.)

.

Develop an object interface layer that more easily supports lookup and storage of objects from standard Java collections (like HashMaps), to be used from within Listeners or Native Peers to access and manipulate JPF objectsMedium/Hard2TBDExperience with Java and OO design important here.

.

Develop string extension to the symbolic execution framework (symbc), with the goal of detecting security problems in Web applications. Medium/Hard1Corina PasareanuExperience with Java; knowledge of decision procedures/constraint solvers a plus.

.

Robustify the existing assumption generation for UML state charts, and then develop a framework for fully automated compositional verification of state charts.Medium/Hard1Dimitra GiannakopoulouThis builds on the existing compositional verification work in JPF (so it is not as hard as it might sound.)

.

Distributed JPF. a new distributed mode that can delegate the state
storage to an external machine which doesn't even have to run Java,
so that JPF can run (almost) in constant space on a workstation.
Medium/Hard1This will require some changes (mostly of the pooled objects), but Peter Dillingers state management provides the basic front end abstractions for it.

.

Generate method sequences for testing. Could include state-matching to reduce the exploration space in between methods. Generate JUnit test wrappers for the tests.Medium2

.

Add parameterized unit tests to JPF's symbolic execution packageHard

.

Mock object support with capture/replay at the unit level.Medium/Hard

.

Assertion generation for unit/regression tests.Medium1

.

Robustify symbolic execution framework (symbc) by incorporating multiple decision procedures/constraint solvers.Medium/HardCorina PasareanuExperience with Java; knowledge of decision procedures/constraint solvers a plus.

.

Extend symbolic execution framework (symbc) to handling input arrays and data structures (by using "generalized symbolic execution" [TACAS'03]).Medium/Hard2Corina PasareanuExperience with Java; knowledge of decision procedures/constraint solvers a plus.

.

Extend symbolic execution framework (symbc) to generating test sequences (in addition to test vectors) for testing Java containers/ UML statecharts (using JPF's statechart extension).MediumCorina PasareanuExperience with Java; knowledge of decision procedures/constraint solvers a plus.