The Java Pathfinder project (JPF) was initially conceived and developed at NASA Ames Research Center in 1999. JPF was open sourced in April 2005 as one of the first ongoing NASA development projects to date, and it is now released under the Apache license, 2.0. JPF is a highly extensible Java virtual machine written in Java itself. It is used to create a variety of verification tools ranging from concurrency software model checkers to test case generators using symbolic execution. JPF is a research platform and a production tool at the same time. Although JPF has major contributions from companies and government agencies, our main user community is academic - there are ongoing collaborations with more than 20 universities worldwide. The JPF team for GSoC 2018 includes researchers from NASA Ames Research Center, Fujitsu Laboratories of America, Royal Institute of Technology - Sweden, Carnegie Mellon University , University of Minnesota, Stellenbosch University - ZA, Charles University - CZ, Teesside University - UK, University of Nebraska–Lincoln.
JPF is designed to be extensible. There are well-defined extension mechanisms, directory structures and build procedures, which keep the core relatively stable and provide suitable, well separated testbeds for new ideas and alternative implementations. As a consequence, there exists many different extensions of JPF that capture different functionalities, including verification, testing, debugging, program repair and security analysis.
JPF has been used for a variety of application domains and research topics such as verification of multi-threaded applications, graphical user interfaces, networking, and distributed applications. In addition to its continued presence in academia, JPF has matured enough to support verification of production code and frameworks such as Android. JPF is constantly being extended with support for verification of new types of properties and for new types of application domains.
- Twitter: JPF is written in Java, and it analyzes Java bytecode. The minimum required skill is to be familiar with the Java programming language. Note that not all projects require a deep understanding of Java or JPF. Please look at the project descriptions to determine which skills are most important.
JPF is a software verification tool. It is a customizable virtual machine that enables the development of various verification algorithms. It will be to your advantage if you are familiar with formal methods, software testing, or model checking. However, JPF is where research meets development, so for many projects not being familiar with formal methods is not a show stopper. We are looking for students who are highly motivated, bright, willing to learn, and love to code.
You can find some project ideas on our project ideas page. Please note that this list is not exclusive. If you are interested in a project that is not listed here, and it is relevant to JPF, we would love to hear about it. You can either email it to us or share your idea in our mailing list. If you have any questions or suggestions regarding JPF and the GSoC program do not hesitate to email us. Join our IRC channel #jpf on freenode to engage in a discussion about JPF.
In order to apply to our organization, you need to submit a proposal to Google during the student application phase (03/12 - 03/27). Check out the GSoC FAQ page for more information.