Java Pathfinder Team
Programming languagesJPF is a Java VM used to verify and debug software
Get involved
Links from the organization’s published listing (2026). Older contact links may have moved.
Proposal examples
Browse the proposal library →Outcomes are reported by the linked archives.
- 2024 · acceptedModel-based-testing-with-Modbat-and-JPF Harshvardhan ↗
- 2025 · acceptedGSoC Proposal JPF SAIF ALI KHAN ↗
- 2025 · acceptedTheJPFTeam RehanChalana GSOC25 ↗
Programs & participation
15 records across 1 programIndexed project records; missing years are not zero. Coverage
2026Google Summer of CodeAnnual program · 2 projects indexed
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2025Google Summer of CodeAnnual program · 3 projects indexed
- Support Java 11/17 for JPF extensions
- Support portfolio of solvers in SPF
- Support Runtime Exception In SPF
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2024Google Summer of CodeAnnual program · 3 projects indexed
- Model-based Testing with Modbat for JPF
- Support for Java 17 for jpf-core
- Support the generation of violation witness in graphML format in SPF
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2023Google Summer of CodeAnnual program · 2 projects indexed
- Better Java 11 Support for Java Pathfinder
- Support Java 11 (bootstrap methods and other issues) for jpf-core
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2022Google Summer of CodeAnnual program · 2 projects indexed
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2021Google Summer of CodeAnnual program · 3 projects indexed
- Improved Integration of String Solvers in SPF
- Systematically explore bit-flip faults in user-specified variables in Java programs
- Using Lightweight Specifications with Fuzzing and Symbolic Execution to Reveal Security and Semantic Bugs
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2020Google Summer of CodeAnnual program · 6 projects indexed
- A Restructuring of the Path Constraint Interface
- Extending Path Merging for SPF
- LyFix: Regression Error Repair for Java Program
- Support Java 11 for jpf-core
- Support Java 11/12 for jpf-core
- Symbolic PathFinder for Neural Network Analysis
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2019Google Summer of CodeAnnual program · 6 projects indexed
- Boosting data race detection by extinguishing state explosion
- Checking Assertions with Symbolic Pathfinder
- Dynamic Partial Order Reduction Engine connected with Symbolic Data Race Detection for Habanero Java
- NFix
- Parallel implementation of Java Pathfinder Project
- Support gradle for jpf-core and extensions.
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2018Google Summer of CodeAnnual program · 4 projects indexed
- Extending Veritesting In SPF
- Modernizing the Java PathFinder Build Workflow: Migrating from Ant to Gradle
- Support Java 9 for JPF-CORE
- Synthesis to repair heap-manipulating programs using Java StarFinder
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2017Google Summer of CodeAnnual program · 7 projects indexed
- Increasing SPF Performance with Bounded Static Symbolic Execution
- Java StarFinder: Symbolic Execution with Separation Logic for Testing and Verifying Heap-manipulating Programs.
- jpf-nas
- Optimize GREEN’s caching for satisfiability and model counting when using SPF
- Program Repair via Symbolic Execution-Derived Constraint Characterization
- Verification and Testing of Heap-based Programs with Symbolic PathFinder
- Visualization of Execution Traces
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2016Google Summer of CodeAnnual program · 10 projects indexed
- Cache layer for jpf-nhandler
- Extending SPF with handling of symbolic arrays, and implementing a replay module
- Fingerprinting for Programs
- Improving JPF Inspector
- Java PathFinder for Android Devices
- Oracle-Based Program Repair
- PSYCO for Reactive Systems
- Using JPF to efficiently compute workload in Multi-Agent Systems
- Verifying Safety of NextGen Models
- Visualization Support for JDart
Source checked Sep 28, 2026
Participation imported from the GSoC Organizations archive snapshot; this historical listing is not an application-status claim.
2013Google Summer of CodeAnnual program · 15 projects indexed
- Abstract Model Checking
- An Eclipse Plug-in for Library Specifications Learning through Testing and Model Checking
- Analysis of biological models in Symbolic PathFinder
- Automated Model Generation for Library Code
- Combining JDart and Randoop
- Computing Observable Modified Condition/Decision Coverage
- Habanero Deadlock Detector
- Human assisted Parameterized Unit tests for GUI Testing
- Invariant Discovery
- Java Platform Debugger Architecture for Java Pathfinder
- JPF as Concurrency Teaching Assistant
- Secure Information Flow by Symbolic PathFinder
- Verification of LTL properties of Java code
- Verifying Probabilistic Programs
- Visual JPF
Source checked Oct 2, 2026
Community mirror of the 2009–2015 Google Melange project archive. Original Melange project links may now redirect; the participation source retains the mirrored records. Organizations without indexed projects may be absent. Imported and normalized from Vaibhav Gupta / GSoC-Data-Analyser, MIT.
2012Google Summer of CodeAnnual program · 11 projects indexed
- Abstract Model Checking
- Conformance Checker
- Dimensional Analysis of Physical Units
- Human Automation Interaction Patterns
- jpf-android: analysing Android applications.
- jpf-qif : Quantitative Information Flow Analysis for Java Bytecode
- Model Checking Android Applications
- Sanitizer validation using symbolic execution and library cross-checking
- Security policy verification via information flow analysis
- Semantic Porting Analysis based on JPF Regression DiSE and DSE
- Trace Server
Source checked Oct 2, 2026
Community mirror of the 2009–2015 Google Melange project archive. Original Melange project links may now redirect; the participation source retains the mirrored records. Organizations without indexed projects may be absent. Imported and normalized from Vaibhav Gupta / GSoC-Data-Analyser, MIT.
2011Google Summer of CodeAnnual program · 11 projects indexed
- Backtrackable FileSystem
- Checking Human Machine Interactions
- Checking Java Annotations
- Detecting Infinite Loops
- Effective representation of symbolic execution tree for SPF
- Generate JPF option lists from code
- Improving Error Discovery of the Slicing and Dicing Technique
- jpf-bdd, A jpf project for handling Boolean variables with Binary Decision Diagrams
- JPF-InspectorII
- JPF-Regression: Extending DiSE for Inter-procedural Analysis
- Support for new Java concurrency primitives & Extending support for Java 1.5 concurrency constructs
Source checked Oct 2, 2026
Community mirror of the 2009–2015 Google Melange project archive. Original Melange project links may now redirect; the participation source retains the mirrored records. Organizations without indexed projects may be absent. Imported and normalized from Vaibhav Gupta / GSoC-Data-Analyser, MIT.
2010Google Summer of CodeAnnual program · 8 projects indexed
- Checking Human Machine Interactions
- Checking Java Annotation
- Construction of Linear Temporal Property verification extension
- Coverage Visualization
- Customizable Trace Server
- Extending String analysis in Symbolic Java Pathfinder
- LTL verification in JPF
- The JPF Inspector
Source checked Oct 2, 2026
Community mirror of the 2009–2015 Google Melange project archive. Original Melange project links may now redirect; the participation source retains the mirrored records. Organizations without indexed projects may be absent. Imported and normalized from Vaibhav Gupta / GSoC-Data-Analyser, MIT.