Research Center for Software Verification
Since JAIST was established, JAIST is working on "research education" and "verifiable and evolvable e-society" projects (activities). Through out these activities, JAIST has the powerful research groups that are formed for software verification in Japan. Research Center for Software Verification (RCSV), evolve from the activities of this group, with the aim to develop a world-leading research, was found in April 2010.
Currently in JAIST, with respect to software verification has been successful conduct of variety of research themes as follows:
- Algebraic Logic, Sub-structural Logic, Modal Logic
- Constructive Mathematics, Intuitionist Logic, Reverse Mathematics
- Algebraic Game Theory, Algebraic System Biology
- Formal Specification Language CafeOBJ and use it for Specification Verification Method
- Integrating Verification Method of Interactive Theorem Prove and Model Checking
- Hybrid System Theory and Speed up Method of Hybrid System Theory Design, Verification Algorithm
- Security Analysis of Large-scale Web Application, Round-off Error Auto-Analysis of DSP Decoder in Embedded System, Auto-termination proof
- Formal Verification Method of Real-time Operating System and Supporting Tool
Based on the above research outcomes, Research Center for Software Verification plans to deploy a comprehensive study on the following themes.
- Verification Logic: Provability logic, etc. to discuss the necessity and logic which underlying a new generation of verification technique.
- Verification Mechanism: Model checking, theorem proving, program verification and variety of code verification mechanism such as rewriting.
- Modeling, Formal Specification Language: The language for modeling the problem and system in the real world and formalizing as formal specification, and verification methods of problem, requirement, specification and design.
- Real-time, Hybrid System: real time, parallel and a hybrid network system, or a verification technology for protocol.