Model checking for distributed systems is a difficult problem today. Several endeavors exist in the research community and industry, but most of them require the instrumentation or abstraction of some key standard libraries.

We focus in our work and in this internship on the JPF model checker for Java programs. JPF is a very attractive tool as it executes bytecode directly, rather than building a model first. One issue with distributed systems is that most of them exploit the new IO library of Java, which is not yet supported by JPF. Several research projects in the world, including ours, would greatly benefit from having JPF be equipped with this java.nio library.

The goal of this internship is then to build with us a JPF extension to support java.nio. The work is essentially about Java and this library, with the potential to publish the extension to the JPF project. Additional goals based on this library are to support UDP and multicast communications, if time allows in the frame of this internship.

• Proficient in the Java programming language.
• Past experience with network programming (socket-based and/or selector-based) in Java or C/C++.
• Available from 3 to 6 months.
• Good command of English.

Applications are managed by NII in the frame of its internship program. The most important point is that applications are through the candidate's home institution, which must be an "MOU partner" of NII. See the official page for detail: Second call for internship for 2010

The internship is co-supervised by Cyrille Artho from AIST and Eric Platon from NII. Please feel free to get in touch for further information.