Centralization of Java bytecode

-- Merging several Java programs into one program

Distributed systems consist of multiple processes. Many analysis tools, like debuggers, support only one process, though. It is therefore interesting to transform multiple processes into a single process, and execute the result in a debugger. This transformation is called Centralization.

Centralization of Java bytecode can be automated, but current tools are based on outdated technology, and no longer work on current Java bytecode. The goal of this internship is to analyze current papers and tools, and build a new centralization tool based on the ASM bytecode manipulation toolkit.

Manipulation of Java bytecode requires interest in, and knowledge of, bytecode or similar machine code, and how program executables are structured into executable code and data. The resulting tool could transform any standard Java program and have a potentially widespread usage, extending the scope of many existing tools such as debuggers.

Requirements

Candidates to this internship should fulfill the requirements below:

• Proficient in the Java programming language.
• Interest or experience in the manipulation of bytecode or object/assembly code, and code generation techniques.
• Available from 3 to 6 months.

Master-Slave Model Checking in JPF

Concurrent software is complex to analyze, because classical testing may miss bugs. So-called software model checkers can analyze all possible outcomes of concurrency, making them a powerful tool to verify such software.

Java PathFinder (JPF) is a software model checking tool. It is basically designed for a stand-alone program. Let us assume that we want to model check a program (SUT -- system under test) that communicates with another program (Peer). The main problem is backtracking: the SUT is backtracked by the model checker, but the Peer does not know that, resulting an inconsistent status between the two programs. To overcome the problem we have developed several techniques, using the cache and checkpointing technologies. There, we have had an assumption that the Peer can be written in any language. However, in our Hadoop verification project, we can assume that not only the SUT but also the Peer is written in Java. In this case, we should be able to use JPF both in the SUT (as Master) and in the Peer (as Slave). In this project, we develop an extension to JPF to achieve this Master-Slave model checking. If time permitting, some ideas for performance improvement will also be realized.

• Proficient in the Java programming language.
• Past experience with multi-threaded programming and network programming in Java
• Available from 3 to 6 months.