Latest JPF News

10/14/2011	A hands-on JPF tutorial will be held on Nov 7th at Lawrence, Kansas co-located with  ASE 2011
05/26/2011	JPF Workshop is co-located with  ASE 2011, Lawrence, Kansas - Submit papers on your work
03/25/2011	JPF student proposals accepted for GSoC 2011  announced - Congratulations to the students
03/18/2011	JPF has been accepted as mentoring org. for GSoC 2011. Visit our ideas page
11/30/2010	JPF version 6 released - update your jpf-core
09/20/2010	ASE 2010 Tutorial on Automated Component-Based Verification Slides
08/02/2010	summer project presentations set for 08/13/2010 - see summer summit event page
04/29/2010	Selected summer projects announced
02/14/2010	ISSTA 2010 Tutorial on Automated Testing with Java PathFinder announced
02/12/2010	Call for Google Summer of Code 2010 project proposals out - visit our SoC page
01/30/2010	JPF Google group replaces old mailing lists
01/12/2010	Fujitsu press announcement released about using and extending Symbolic PathFinder (projects/jpf-symbc) for comprehensive testing of Java web applications
09/02/2009	JPF server on http://babelfish.arc.nasa.gov/trac/jpf goes live, featuring the JPFWiki and separate Mercurial repositories for JPF core and extension projects
07/22/2009	JPF wins the 2009 "Outstanding Technology Development Award" of the Federal Laboratory Consortium (FLC), Far West Division

Welcome to the JPF Wiki

This is the main page for Java™ Pathfinder, or "JPF" as we call it from here. JPF is a highly customizable execution environment for verification of Java™ bytecode programs. The system was developed at the  NASA Ames Research Center, open sourced in 2005, and is freely available from this server under the  NOSA 1.3 license.

The JPFWiki is our primary source of documentation. It is divided into the following sections (which you will always see in the TOC menu to the right):

• What is JPF? -- a brief introduction into JPF and what sets it part from normal testing
  • software model checking examples (as one possible JPF application)
• How to obtain and install JPF -- everything to get it running on your machine
  • System requirements
  • repository access from shell, Eclipse? or NetBeans?
  • installing the Eclipse or NetBeans plugins
• How to use JPF -- essentially the user manual for JPF
  • JPF application types and runtime components
  • configuring and running JPF
  • understanding JPF output
  • using the Verify API
• Developer guide -- what's under the hood
  • the toplevel design
  • key mechanisms like ChoiceGenerators and partial order reduction
  • extension mechanisms? like Listeners, Search Strategies?, Model Java Interface (MJI), Bytecode Factories, Property checks?, Publishers?
  • running JPF from within your application
  • directory structure? and coding conventions
  • writing JPF tests
• Projects -- descriptions of available JPF projects and repositories
• Related Research and publications
• About -- how are artifacts and work organized
  • About this Wiki
  • About the Development Process?
  • About the source repositories?
  • How to contribute
  • How to get a JPF contributor account
• FAQ -- answers to all your questions (eventually)
• History? -- how did we get here
• Support -- who supports this project
• People? -- who does or did contribute
• News? -- what's going on right now
• Future Plans? -- where do we want to go

---

^{Java and all Java-based marks are trademarks or registered trademarks of Sun Microsystems, Inc. and its subsidiaries in the U.S. and other countries}