The Java Pathfinder Team

Mentors: Student: Soha Hussein

<p>Path merging is a promising technique that speeds up dynamic symbolic execution by multiple factors. In Path merging expensive forking is minimized by statically analyzing and summarizing regions of code, which are then used during dynamic symbolic execution. This technique was first introduced by the name of Veritesting[1] for c programs and recently implemented for Java programs in Java Ranger [2]. Both works report substantial benefits from merging of paths, with the latter winning SVComp’2020, a competition among Java verification and analysis tools.</p> <p>In this proposal, I plan to: 1) support test case generation for Java Ranger that would support branch coverage criteria, and 2) experiment the feasibility of path merging of threads by implementing a simulated thread interpreter and using Java Ranger to path merge thread interleavings.</p>

Mentors: Student: Yuvaraj Anbarasan

<p>JPF is a model checking tool for Java applications. It is a Virtual Machine (VM) for Java bytecode which executes the system under test (SUT). The JPF source is partially compatible with Java 11. The problem is to support new features of Java 11 like the bootstrap methods. They are used for things as common as string concatenation ( String + String, String + int, String + double, String + Byte, etc ). As of now, a few specialized cases are supported, but there are still few cases that fail with Java 11. There are also some internal APIs from Java 11 that no longer exist in Java 12. Therefore the aim of this project is to support the general case of bootstrap methods and update the code to support java 12.</p>

Mentors: Student: Quang-Cuong Bui

<p>Automated Program Repair (APR) has been showing a high capability recently of fixing software bugs automatically. Despite the recent advancements, there are only a few APR techniques specifically addressing regression errors. These techniques yet, however, have not fully exploited the information available in software evolution history, e.g., bug-inducing commits, etc, for repairing regression errors. Moreover, the techniques either work on a specific language (e.g., C language) or do not provide their implementations for public access.</p> <p>This project aims to empower automatic repair of regression errors for Java programs by implementing and extending recent interesting findings of regression errors, e.g., the correlation between bug-inducing and bug-fixing commits. We aim to build a system, namely LyFix, that enables users to fix Java regression bugs automatically by leveraging fix ingredients and specific repair operators learned from the software development history.</p>

Mentors: Student: Carson Smith

<p>SPF’s constraint interface needs to be restructured. The current implementation doesn’t allow for the easy addition of new solvers and could be optimized further. In order to do so, I propose the creation of a new hybrid list-tree data structure for the constraints of a path, roughly similar to that of the Abstract Syntax Tree utilized by the GREEN framework with the help of the visitor pattern. With this sort of data structure, SPF’s key backtracking features that allow for symbolic execution would remain intact, while the design of the constraint library would gain a level of abstraction that is not currently implemented in the code.</p>

Mentors: Student: Amgad Rady

<p>JPF does not yet fully implement the features of Java 11 - support extends only to Java 8 - including features as simple as string concatenation. This is an especially difficult situation given that Oracle has initiated an “end of public updates process” for Java 8 (although it is interesting to note that Oracle will continue “premier support” for Java 8). It is likely that many Java users will migrate to higher versions, and unless JPF fully supports the new features of a higher version of Java it is unlikely to be used and adopted.</p> <p>A crucial feature of Java 11 that needs to be urgently implemented is support for bootstrap methods that are generated and resolved at load time. These are used in Java for things as varied as string concatenation and lambda expressions. It is likely that more features of Java will take advantage of bootstrap methods as we go forward, so it is desirable to have a complete bootstrap method resolution engine in the JPF runtime that complies with the Java Virtual Machine 11 (JVM 11) specification for JPF to remain current.</p>