In the summer of 2016, I participated in the Google Summer of Code program, during which I updated and significantly improved the Java Pathfinder Inspector.
Java Pathfinder (JPF) is a framework for formal checking of Java programs. Its core consists of a virtual machine for Java bytecode, running itself on Java; this allows JPF to instrument the code and provide its own functionality for critical instructions. JPF is very extensible and many modules exist for various kinds of verification such as symbolic execution. JPF Inspector is one such JPF module that focuses on debugging capability.
JPF Inspector is a tool for inspection and control of Java Pathfinder execution. It supports breakpoints and single-step execution (forward and backward) at different levels of granularity, and it allows the user to examine and modify program state (threads, call stacks, and heap objects). Unlike with standard debuggers (GDB), it is also possible to control thread scheduling explicitly.
This is the first software engineering project for which I received actual money.
It is programmed in Java.
It was created at the age of 23, in 2016.
Links:
- Primary GitHub repository
- Primary documentation
- GitHub repository I used during the summer of 2016
- List of my most major additions/changes
- Java Pathfinder main website
Selected major additions of mine (full list):
- Extensibility: custom commands, aliases and hit conditions
- Command-line mode
- Explorer view, source code view, quick commands
- 10 new commands and 9 new hit conditions
- Very detailed documentation