What follows is not a complete list of activities, but gives you a good idea as to what has been going on.

Since then I/we (Joe & UCD) have been:

• coordinating with Mobius partners and other collaborators on tool design and development,
• identifying core features of the Mobius Integrated Verification Environment (IVE),
• identifying and reviewing potential reusable code bases,
• comparing foundations for tool development, and
• running a sporadic "verification bootcamp" at UCD to get my Ph D^? students up-to-speed on the core features of verification systems in general.

We plan on starting, after mid-May, the following activities, to which Mobius partners and other collaborators will be invited:

• organize site visits for key personnel for tool design, development, and integration. Such visits are already beginning in two weeks with visits from Julien Charles, Aleksy Schubert and, later we hope, Mariela Pavlova.
• running regular online design meetings focusing on specific subsystems,
  • these meetings will be some combination of vidconf, Skype, IRC, iChat AV, and VNC communication technologies.

The current tools that are under development for Mobius includes:

• the BML work at INRIA,
• a lightweight prover interface plugin (UCD + INRIA) that supports Coq and PVS,
• a lightweight static concurrency checker (UCD),
• an immutability checker (UCD),
• the Umbra bytecode editor plugin (Warsaw),
• a beta release of ESC/Java2 (UCD and many others),
• a new JMLEclipse plugin (KSU and UCD),
• a new ESC/Java2 plugin (KSU and UCD),
• an integrated build, test, version control, and reporting framework (UCD),

More subprojects will start up in Summer. These will include further work on the BML (as discussed in Marieke's recent email), implementing a Boogle PL^? subsystem (at least, that looks like where things are heading, given recent emails from Peter that I need to answer), integrating newly updated ESC/Java2 and U.S. tools (e.g., RCC, Houdini, Daikon, Bogor, etc.), etc.

It also looks like we will have to take over/restart development on the JMLEclipse and ESC/Java2 plugins and the JML3 foundation (conjointly with Patrice Chalin's group at Concordia). We simply cannot depend upon an external team (KSU, in this case) for critical components, so we'll have to push the development ourselves.

As we have also just won an Enterprise Ireland travel grant that will send UCD Mobius personnel and collaborators to the U.S. this Summer for a few weeks. In particular, we'll be visiting Michael Ernst and others at MIT, Jason Hickey and others at Caltech, John Hatcliff and others at KSU, and (likely, short visits to see) Gary Leavens and Cesare Tinelli to facilitate the above work.

To coordinate this activity we have been using the SRG wiki as a local sandbox for Mobius IVE analysis and design. We plan on making "snapshots" of this wiki web regularly (and perhaps automatically) from the UCD wiki to the Mobius wiki (or, more specifically, the Tool web in the Mobius wiki). We are also using a local GForge to coordinate this activity locally, but plan on moving that activity to the Mobius GForge so as to provide a more public, "partner-visible" face to Task 3.6.

As I have administrator access to the Mobius wiki and GForge, I am happy with our level access and control for those resources.

My biggest difficulty has been finding a postdoc candidate with the appropriate level of expertise that can help with these activities. I have received several quality applications from theoreticians who have no real software engineering skills, but only one person rides the delicate boundary between theory and practice. He'll be visiting Dublin and interviewing in the 3rd week of May. If I cannot find an appropriate candidate I am going to suggest we recast the position as a research programmer.

-- JosephKiniry - 18 Apr 2006