Google Summer of Code 2025

"Open source is not just about code; it's about community, learning, and contribution."

Hey everyone!
I’m Saif Ali Khan, a BCA graduate from Dayanand Academy of Management Studies, Kanpur. This summer, I’m excited to be a part of Google Summer of Code (GSoC) 2025, contributing to The JPF Team under a project titled:

“Support Runtime Exceptions in Symbolic Pathfinder”

It’s been a challenging experience so far. This post shares my progress at the halfway point as the midterm evaluation is close. One thing to add, my mentor is really nice and kind; she helps me whenever I am stuck on something.

📦 About the Project

Description: The main goal of this project is to support throwing a runtime exception for some of the summarized functions such as String.contains(). This project extends the SPF branch sv-comp.

Difficulty: Medium Scope: 350 hours
Required skills: Knowledge of Symbolic Pathfinder

To understand SPF, we need to know a little bit about JPF (Java Pathfinder). It is a model checker. What is model checking? It is a formal verification technique that specifies whether a finite-state machine of a system satisfies a specification or not. JPF also has an Abstract Virtual Machine; it does not execute a program like a normal JVM. Instead, it systematically explores all possible execution paths to check for errors, deadlocks, and unhandled exceptions. JPF was started as a model checker around 1999 and was developed at the NASA Ames Research Center.

JPF also has extensions like Symbolic Pathfinder (SPF), which combines symbolic execution with model checking and constraint solving for automated test case generation and error detection in Java bytecode. In SPF, programs are executed on symbolic, rather than concrete, inputs.

String str;

In the above example, the String variable can be null, can be my name, can be your name, anything. So currently, I am working on this project.

🤝 Community Bonding Period

Before the coding began, I spent time getting familiar with the project and community. Here’s what I did:

🧑‍💻 Attended two meetings:
- One for onboarding and orientation
- Another focused-on project setup and tooling
🛠️ Set up the development environment with mentor guidance and ran initial builds/tests.
🔍 Explored the codebase and understood how things are working; it was very overwhelming.

Development Environment

IntelliJ IDEA Ultimate
Java 8
Gradle 6.9
Ubuntu Jammy

I was asked by the mentors to set up and clone the project on my machine. The SPF, the benchmark-defs, and the setup for the benchexec tool were very overwhelming because I was getting errors for cgroups on Ubuntu when I ran the benchmarks on the SPF zip. I figured things out by following my mentor's guide and the README on the repos, and I was able to set up the project and run it successfully.

What is sv-comp? It is a Software Verification Competition that happens annually and evaluates the effectiveness of software verification tools. It provides a set of verification tasks to compare different tools for security, correctness, safety, etc. SV-BENCHMARKS are the collection of these tasks, including programs written in languages like C and JAVA. These benchmarks help in assessing the performance of verification algorithms.

👨‍💻 Coding Period

Here’s a breakdown of what I worked on:

🔍 Task 1: String & StringBuilder Support Mapping

My mentor first asked me to:

Analyze which String and StringBuilder functions are supported or unsupported in SPF and what Runtime Exception they can raise.
I compiled this into a Google Sheet, making it easier to track progress and limitations in symbolic string support.

📊 Task 2: Benchmark Failures in SV-COMP

We noticed that 278 benchmarks were giving incorrect false results in the SV-COMP suite, significantly affecting our score.

I was asked to:

Go through each failing benchmark
Identify which exception can be thrown (e.g., NullPointerException, IndexOutOfBoundsException, etc.) for the Runtime Exception property.
Document this to help with debugging and fixing the underlying causes

Before that, I tested SV-COMP benchmarks on:

The old SPF version (submitted ~2-3 years ago)

This helped us pinpoint regressions and behavior changes between versions.

🧵 Task 3: Investigating Symbolic String Creation

My mentor asked me to:

Find where symbolic strings are created in the codebase
I traced this to a specific file and instruction handling point.

Initially, I added a null-check right after the symbolic string creation in the SymbolicListener, but it wasn’t effective because:

The native return was not executing twice.

🔧 Final Fix: Moving Logic to Symbolic String Handler

To solve this:

We shifted the logic into the SymbolicStringHandler
Now, the symbolic string has three execution paths:
1. One for null
2. One for the if branch
3. One for the else branch

This finally worked as expected and is helping improve symbolic string coverage and path exploration!

Currently, contains() has support for these three choices. Further, I will be working on the IFNULL JVM instruction.

🔗 Contributions & Pull Requests

✅ Merged PR: Improve max/min to handle NaN, -0.0f/-0.0d correctly
🕓 Open PR (Under Review): Add missing null choice (0) in symbolic string handling (fix:) GSoC'25

🏁 Wrapping Up

This first half of GSoC has been both intense and rewarding.

While the progress may seem gradual, it's important to understand that working deep within the JVM, especially with tools like Symbolic PathFinder, is no walk in the park. You’re dealing with bytecode, native methods, symbolic execution, and internal instruction handling, where even small changes can affect hundreds of execution paths.

Debugging at this level isn't just about writing Java — it's about understanding how the JVM thinks.

Despite the challenges, while coding, I have learned a lot from my mentors and from some articles.
(PDF) Symbolic PathFinder: Integrating symbolic execution with model checking for Java bytecode analysis

Thanks for reading! 🙌

🚀Google Summer of Code 2025: The JPF Team's Symbolic Pathfinder

Table of contents