JPF News
- 05/03/08: Another JPF workshop come and gone. We just had two
exciting days packed with topics from all over JPF, including interesting
applications like Fujitsu's WEAVE framework for checking web applications, and
the AgentJPF project from Universities of Liverpool and Durham, UK. Slides are still
coming in, but - in case you weren't there - you can already see what you've missed
on the event schedule page.
Thanks to our hosts from Fujitsu and to all participants for making this such
a successful event.
- 04/15/08: Google Summer-of-Code projects selected. It appears we didn't
even report on that one: JPF was selected for this years
Google's summer of code. We got a
huge number of propsals, of which we were able to select 10. It could have been
more, but we ran out of mentors. Welcome to the new contributors, we are looking
ahead to an exciting summer.
- 04/04/08: Fujitsu announces WEAVE framework. Fujitsu Japan issued a
press announcement regarding their
WEAVE framework for verification of web applications. This is great news
since it shows JPF is making it's inroads into industrial applications, which
is esp. important since this is such an important application domain.
- 02/01/08: Workshop dates set. We will have a two days workshop
on 05/01 and 05/02 at the Fujitsu campus in Sunnyvale, CA. Tentative plans are
to have "what is being done with JPF" presentations the first day, and
reserve the second day for general and specific JPF questions, BoF's and
whatever might come up. Please have a look at the
event web page
and contact Peter Mehlitz at
<Peter.C.Mehlitz "at" nasa.gov> if you are interested to attend or give a talk.
- 10/23/07: More awards - Corina and Willem won the
HVC 2007
award for their work on symbolic execution with JPF. Congrats! That was even
still the "old" symbolic execution mode (using translation), so there's more
to come...
- 08/20/07: It's been a while, but the silence wasn't due to a lack
of JPF progress - rather the contrary. The pure Java, non-intrusive symbolic
execution for test case generation now comes into prime. We also have been
busy with the UML statechart model checking extension, and with adapting the
compositional verification algorithms to JPF. The action now shifts from the
JPF core to extensions and tools.
- 05/22/07: We just had a very successful collaboration with Fujitsu,
pushing the scalability envelope by finding a deadlock involving 18
threads in a very large application, all at a search depth of >1000.
Not bad for an afternoon (of running JPF). This also introduced a
nice addition to the tools: the DeadlockAnalyzer (to analyze large
traces of concurrency operations). Here is the official Fujitsu announcement:
"The Java Pathfinder model checking tool architected and developed at
NASA AMES Research laboratories was used to detect bugs in an internal
Fujitsu code base that ran into one million lines of Java code. First
the application was converted into a fully executable stand-alone Java
model. With the active support of the NASA AMES team, the researchers at
Fujitsu laboratories of America (Sunnyvale) and Fujitsu Laboratories
Limited (Kawasaki, Japan) were able to uncover injected (seeded) bugs in
the application model that sent the model into panic mode. In this
process the Java Pathfinder tool explored approximately 125,000 program
states and millions of paths which would be impossible to cover using
conventional testing techniques. The tool also uncovered an unexpected
deadlock situation in the application model."
- 02/01/07: Willem leaves the ship while it's picking up speed!
But he is not abandoning JPF and will stay in touch with the team. After all,
he has been involved for too long to ever get rid of it. We wish him good luck
at SEVEN Networks, his new company
- 11/21/06: Some reorganization - the state abstraction has been moved
into the core, and extensions have to be built explicitly. The theoretical
rationale is that extensions might need special build procedures (hence they
have their own build.xml), or they might replace core functionality in ways
incompatible with other extensions (you better have a good reason for it!).
As a welcome side effect, this will make it easier to detect when hidden
dependencies of the core on specific extensions sneak in.
The real reason? Well, the action is shifting towards the
extensions (lots of construction sites like UI model checking, statechart
model checking, and more exciting things in the making), so we need to
clean ship
- 06/30/06: JPF v4, finally! After a long period of silence due to
other assignments, we finally pulled all the pieces together to get
JPF4 out of the door. The major achievements are
ChoiceGenerators and
Java 5.0 compatibility, but there are many others (numerous bug fixes,
reflection support, instruction interception etc.). Configurable state
management (esp. matching) is now also in the works - the last missing extension
mechanism. And while we were at it, a lot of the sources have been converted to
use Java 5.0. Great work by our summer interns, esp. Peter Dillinger.
- 24/02/06: Join the JPF community on Frappr:
http://www.frappr.com/jpfusers
- 10/21/05: the documentation is now readable HTML + CSS, which is
not so nice for printing, but everybody can edit and add. The whole
website (w/o experimental Wiki) is now in CVS, only the graphics
sources (which are OmniGraffle *.graffle files) are not. Maybe we
add them as SVGs at some point (but OminiGraffle doesn't load them
yet).
- 10/08/05: switched from MD5StateSet to Peter Dillinger's
JenkinsStateSet, which is up to 25% faster on some (large) examples.
Great contribution
- 09/08/05: the data choice generators make their first appearance.
Drop Verify.randomX(..) now
- 08/29/05: JPF should now be Java 1.5 compatible. There might be a
few surprises left in the libraries, but the regression test suite
builds and runs on J2SDK 1.5
- 08/24/05: The JPF tutorial at
labs.com/cm/cs/what/spin2005/">Spin 2005 drew
quite a crowd, despite the late hour on the last conference day
- 04/26/2005: Alast - JPF becomes the first NASA software opensource
project that is hosted on SourceForge! External interest had grown
enough that open sourcing just seemed to be the right step. JPF is still
a moving target, there are exciting ideas to extend it, and so NASA took
the bold step to not just open the sources, but to make further
development a collaborative effort. We have a first! Read the
official press announcement. May JavaPathFinder boldly explore from
where no program has ever returned
- 03/2005: The move to the new configuration and initialization scheme
has been completed. Now everything is configured via a hierarchy of Java
property files that can be overridden from the command line, eliminating
the need to update a central option registry every time a new option is
added in a remote part of the system. Read the online docu to find out
more.
- 01/2005: The JPF Team will present a tool tutorial at the 12th
International SPIN Software Model Checking workshop in San Francisco
(August 2005). More details can be found here
- 11/2004: Fujitsu Labs of America successfully uses JPF to locate
subtle concurrency errors in parts of their enterprise software
- 08/2004: JPF Team receives a Certificate of Recognition for
"creative development of technically significant software" from NASA's
Inventions and Contributions board
- 09/2003: Search- and
VMListeners are added to the extension repertoire of JPF. Hopefully,
this will put an end to ever extending JPF's core classes. Now you can
add your own hyper-search algorithms and most favorite properties
outside the critical core
- 07/2003: The Model Java
Interface (MJI - blame Peter for the bad name) is added to the code
base. Now we can use the same mechanism for core class JPF interaction
and library abstractions (saving states on the way). Mind-twisted things
become possible with this
- 06/2003: Here comes another award - NASA Office of Aerospace
Technology awards JPF its "Turning Goals Into Reality" (TGIR)
Engineering Innovation Award. Read on
- 04/2003: First publication on the
introduction of symbolic execution on top of JPF
- 04/2002: JPF tutorial at ETAPS 2002 in Grenoble, France
- 02/2001: JPF is released by NASA for beta-testing and project
collaborators
- 09/2000: Main conference paper on JPF published at International
Automated Software Engineering Conference ("Model Checking Programs").
It was considered for the best paper award, but narrowly lost out - it
has since become one of the most cited papers (>100) from the ASE
conference series according to citeseer. Journal version of
this
paper is now available in the ASE journal
- 07/2000: First JPF paper published at "Advances in Verification"
workshop
- 12/1999: JPF gets it first outing in public during a presentation at
the LUACTS workshop in Johannesburg, South Africa