Java Pathfinder

This is the main page for Java™ Pathfinder (JPF). JPF is an extensible software model checking framework for Java™ bytecode programs. The system was developed at the NASA Ames Research Center, open sourced in 2005, and is freely available on this server under the Apache-2.0 license.

##

• Introduction - a brief introduction into model checking and JPF <!–* What is JPF?
  • Testing vs. Model Checking
    • Random value example
    • Data race example
  • JPF key features–>
• How to obtain and install JPF - everything to get it running on your machine <!– System requirements
  • Downloading binary snapshots and sources
  • Creating a site properties file
  • Building, testing, and running
  • Installing the JPF plugins
    • Eclipse
    • NetBeans–>
• How to use JPF - the user manual for JPF
  <!– Different applications of JPF
  • JPF’s runtime components
  • Starting JPF
  • Configuring JPF
  • Understanding JPF output
  • Using JPF’s Verify API in the system under test–>
• Developer guide - what’s under the hood <!–Top-level design
  • Key mechanisms, such as
    • ChoiceGenerators
    • Partial order reduction
    • Slot and field attributes
  • Extension mechanisms, such as
    • Listeners
    • Search Strategies
    • Model Java Interface (MJI)
    • Bytecode Factories
  • Common utility infrastructures, such as
    • Logging system
    • Reporting system
  • Running JPF from within your application
  • Writing JPF tests
  • Coding conventions
  • Hosting an Eclipse plugin update site–>
• JPF core project - description and link to jpf-core
• Projects - link to currently active and legacy extensions of JPF
• Workshops - link to annual workshops on JPF
• Google Summer of Code - link to JPF’s participation in the Google Summer of Code program, current ideas page here.
• Mailing list - discussion about JPF takes place in Google Groups JPF Google Group
• Discord - join our Discord server for more discussions

##

Latest JPF News

• 02/28/2025 GSoC 2025: The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the JPF/GSoC page.
• 02/23/2024 GSoC 2024: The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the JPF/GSoC page.
• 07/21/2022 JPF is now on Twitter! Follow us and check out our feed for the latest news and updates.
• 05/13/2022 JPF Workshop 2022 will be co-located with ASE 2022 in the Oakland Center, Michigan, United States. Please consider submitting a paper.
• 03/09/2022 GSoC 2022: The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the JPF/GSoC page.
• 11/23/2021 JPF 2021: The JPF team organizes a virtual JPF day this year! Check our call for participation.
• 03/09/2021 GSoC 2021: The JPF team has been accepted again as mentor organization for the GSoC program! To learn more, please visit the JPF/GSoC page.
• 02/21/2020 The JPF team has been accepted to the GSoC program for 2020! To learn more, please visit the JPF/GSoC page.
• 07/24/2019 JPF Workshop 2019. The workshop will be co-located with ASE in San Diego, CA.
• 02/26/2019 The JPF team has been accepted to the GSoC program for 2019! To learn more, please visit the JPF/GSoC page.
• 05/08/2018 JPF Workshop 2018 will be co-located with FSE 2018 in Lake Buena Vista, FL. Please consider submitting a paper.
• 01/23/2018 The JPF team is applying to the GSoC program for 2018. To learn more, please visit the JPF/GSoC page.
• 05/01/2017 JPF Workshop 2017 will be co-located with ASE 2017 in Champaign, IL. Please consider submitting a paper.
• 02/27/2017 JPF got accepted for GSoC 2017. Please visit our ideas page, and let us know if you have a topic in mind.
• 01/19/2017 The JPF team is applying to the GSoC program for 2017. To learn more, please visit the JPF/GSoC page.
• 06/01/2016 JPF Workshop 2016 will be co-located with FSE 2016 in Seattle, WA, on November 18, 2016. Please consider submitting a paper.
• 04/22/2016 JPF student proposals accepted for GSoC 2016 announced - Congratulations to the students!
• 02/29/2016 JPF got accepted for GSoC 2016. Please visit our ideas page, and let us know if you would like to propose a project.

Old news

• 17/08/2015 JPF Workshop 2015 Accepted Papers are announced. Please visit ASE 2015 for registration, date and venue information.
• 10/03/2014 JPF Workshop 2014 Accepted Papers. Please visit SOAR Lab for registration, date and venue information.
• 10/01/2013 JPF Workshop 2013 Accepted Papers. Please note JPF Workshop 2013 website is down due to the shutdown, please visit ASE 2013 for registration, date and venue information.
• 06/20/2013 JPF Workshop 2013 will be co-located with ASE 2013 Please submit papers.<\li>
• 05/27/2013 JPF student proposals accepted for GSoC 2013 announced - Congratulations to the students!
• 04/08/2013 The show is on - JPF got accepted for GSoC 2013. Please visit the GSoC project ideas page or let us know about your own project suggestions.
• 06/07/2012 JPF Workshop 2012 is co-located with FSE 2012, November 11 and 12. We solicit submissions for the JPF Workshop 2012.
• 04/23/2012 JPF student proposals accepted for GSoC 2012 announced - Congratulations to the students!
• 03/26/2012 GSoC Student Applications period is open until April 6. Please submit your proposal at JPF GSoC page.
• 03/16/2012 JPF has been accepted as mentoring org. for GSoC 2012. Visit our ideas page.
• 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/2010JPF version 6 released - update your jpf-core.
• 09/20/2010ASE 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 for comprehensive testing of Java web applications.
• 09/02/2009 JPF server on 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.
</ul> </details> ##