Research Hightlights for 2005
We make distinctions between two kinds of research: scientific one founded on academic interests and firldwork for the interests of practitioners. We hope that new scientific and technological activities will emerge through conscious interaction of the two.
One of our objectives is to create a functorial semantics of abstraction used in verification of reactive systems. We proposed this fiscal year the logic Rμ and succeeded in constructing a suitable semantics of abstraction with respect to Rμ. The logic subsumes well-known CTL as its sub-logic and is itself a sub-logic of the modal μ-calculus.
We also develop MLAT, a prototype assistant system for automatic sbstraction of pointer-manipulating programs. In MLAT, properties of the heap space where pointers reside are described by a modal logic with the special modalities such as "...holds at the cell". We are proposing a highly original approach to pointer reasoning, completely different from the better-known Separation Logic by J. Reynolds.
Further, we are developing Agda, an interactive proof-assistant system based on Martin-Löf Type Theory. This is a joint effort with Chalmers University of Technology in Sweden.A plug-in mechanism was implemented for systematic coordination between Agda and external verification tools. Using this, we have connected Agda with the model checker SMV and with the first-order predicate logic prover Gandalf. Our goal is to construct Integrated Verification Environment, which combines interactive styles of verification and automatic ones; the plug-in mechanism marked an important first step.
This fiscal year saw a substantial development in our joint research with industrial partners on model-checking technology adoption. Field trials that are more realistic have been conducted at the actual sites of software production. Through this collaboration, we have been developing, and accumulating hands-on experiences on, necessary technologies to incorporate model-checking methods into the software development cycle at the companies.
Also, we have developed training courses on verification using model-checking and interactive theorem-proving. Trials have been conducted for feedbackes and experiments on course management. The four-day model checking training course (introductory level) was run 16 times on a trial basis, and had approximately 70 participants including researchers, students, and system engineers. CVS are now in the process of developing such courses in intermediate and advanced levels to meet the strong demand from those participants. A new four-day interactive verification training course (introductory level) was also stared on a trial basis.
In addition to the above, in October 2005, CVS hosted "2nd Science and Technoogy of System Verification Symposium." Other event CVS hosts indlude bimonthly "System Design Verification Research Consortium" and "CVS/AIST Workshop Series" on irregular basis. These events have attracted numerous participants from both academic and industrial communities.