The JPF team

Mentors: Student: Salmane Khalili

Java-Ranger is a path merging extension of Symbolic Pathfinder, that collapses multiple execution paths into a single region with a disjunctive constraint. Currently, it handles only integer constrains, which means, floating-point (FP) operations are either approximated unsoundly or cause solver errors. In this project, the aim is to add sound IEEE-754 floating-point support to Java ranger, enabling the correct summarization of regions containing FP arithmetic, comparisons, conversions, and library calls. The work heavily involves refactoring the underlying FP support in SPF (Modelling special values, rounding, comparisons, and conversions), then extending Java Ranger’s AST visitors, merging heuristics, and solver integration to handle the new FP constraints. The result will be an engine capable of analyzing FP-Java programs. Deliverables include: - New floating‑point expression nodes in the numeric package. - Updated bytecode handlers for all FP instructions. - Solver integration for Z3bitvector using the floating‑point theory. - Constant folding and simplification passes for FP expressions. - A test suite validating the correctness and coverage of FP handling. - Documentation of the new API and usage.

Mentors: Student: Darshan Raghavendrachari

JPF currently cannot fully analyze Java 17 programs that use sealed classes and records — two features now standard in modern Java. This project completes Java 17 support in jpf-core by fixing sealed class enforcement, adding full record support (classfile parsing, metadata storage, and execution), and producing a Java 17 audit document that maps all remaining gaps for future contributors. The work targets the java-17 branch and builds on an existing contribution to the codebase.

Mentors: Student: Rehan Chalana

Java PathFinder (JPF) is an extensible software analysis framework for java bytecode which can be used to check for concurrency defects like deadlocks, and unhandled exceptions like NullPointerExceptions and AssertionErrors. Symbolic PathFinder (SPF) is its extension that enables symbolic execution of java programs. This proposal outlines my plan to contribute to The JPF Team by working on the Support portfolio of solvers in SPF Project during Google Summer of Code 2025. The main goal of this project is to enable the simultaneous invocation of multiple constraint solvers, where execution halts as soon as any solver returns a satisfactory result. This approach is expected to enhance SPF's ability to handle a broader range of constraints. This Project will extend SPF branch sv-comp. The outcome will enhance SPF’s scalability and applicability in symbolic execution tasks.

Mentors: Student: Mahmoud Khawaja

Java Path Finder (JPF), a specialized Java Virtual Machine for software verification, excels with Java 8 but faces challenges with modern features in Java 11 and 17, such as bootstrap methods (e.g., lambdas and string concatenation) and internal functions like toString() and hashCode() for records. My project seeks to address this by enhancing JPF to fully support Java 11 and 17. I will upgrade BootstrapMethodInfo to manage string concatenation effectively, refine INVOKEDYNAMIC execution to mirror the host JVM’s dynamic call site generation, and ensure internal functions operate correctly for new Java features. Drawing on OpenJDK research, I’ll implement these changes and validate them with thorough testing. Deliverables include full Java 17 support in JPF’s default branch, a comprehensive test suite for string concatenation and records and updated documentation. This work will modernize JPF, enabling it to verify advanced Java programs and strengthening its value to the verification community.

Mentors: Student: Saiff

The main goal of this project is to add support for handling runtime exceptions in SPF that will improve SPF's performance on SV-COMP benchmarks. There are two main reasons why SPF is losing many points in runtime exception verification tasks. First, SPF is not systematically exploring execution paths where symbolic variables could lead to runtime exceptions like NullPointerException and StringIndexOutOfBoundsException, resulting in many incorrect false results where actual exceptions are not detected. Second, the SV-COMP execution script is lacking proper property detection and result classification for runtime exception scenarios. To address these problems, we should extended SPF to have additional choices that will explore potential runtime exception scenarios when symbolic variables could represent values that can raise them. To deal with this, we can analyze why SPF outputs wrong answers for certain verification tasks and fix them. This systematic approach to runtime exception path exploration will help fix SPF's behavior, improving its scores on SV-COMP benchmarks. This project extends the SPF branch, sv-comp.