Formal Verification (National Institute of Advanced Industrial Science and Technology)

Research Staff

Research Areas

Formal verification methods are mathematically rigorous techniques for checking the correct behavior of software and hardware systems. Various techniques and tools for formal verification have been applied to developing, e.g., bug-free programs, secure cryptographic protocols, and reliable operating systems. Nowadays, formal verification is essential for building a trusted and secure digital society. Our group studies formal methods for specifying and verifying software systems with uncertainties involving, e.g., probability, statistics, and physical environments. Our work includes the application of formal verification methods to rigorously verify and explain artificial intelligence systems and statistical programs, and to ensure the safety and security of cyber-physical systems, such as robots. For this purpose, we conduct research on the formalization of mathematics, statistics, programming languages, and related topics in theoretical computer science.

Formal verification using theorem provers

Our primary tools to perform formal verification are proof assistants and automated verification tools. A proof assistant is a software tool that checks mathematical proofs written in formal logic. This checking mechanism is based on research in formal logic and type theory.

Using proof assistants (e.g., Rocq) and automated verification tools, we develop reusable libraries of formal definitions and theorems that can be used to formally represent AI and robotics systems, computer programs, mathematics, and statistics.

Fig. 1 形式検証の概要

Fig. 1 Formal verification overview

Formalization and verification technology for AI and Robots

The behavior of AI and robotics software systems may involve uncertainty, because these systems learn from datasets and interact with the physical environment. Our group conducts research on formal methods to specify, verify, and explain the correctness and safety of AI and robotics systems in uncertain environments.

Current research:

Fig. 2 SCARA robot arm

Fig. 2 SCARA robot arm

Formalization of mathematics

The rigorous verification of software relies largely on mathematical theories. For instance, the formalization of probability theory and statistics is used to verify and explain AI systems and statistical software; the formalization of algebraic methods is necessary to verify robots and functional programs; the formalization of real analysis is necessary to verify the physics of cyber-physical systems.

Fig. 2 SCARA robot arm

Fig. 3 A formal proof in Rocq

Current research:

Key Features

About AIST

AIST (National Institute of Advanced Industrial Science and Technology) is one of the largest public research organizations in Japan. We are affiliated with the Intelligent Platform Research Institute (IPRI) which is in the Tokyo Bay area.

Basic knowledge to start research

  • A strong interest in applications of mathematics to software verification.
  • Basic knowledge in formal logic and in the semantics of programming languages (functional programming languages, type theory, etc.).

Guidance policy

  • We expect students to acquire basic knowledge of formal verification techniques and will then discuss research topics according to the students' interests.
  • We are ready to discuss spontaneous research proposals from students and provide guidance, in English, Japanese, or French.
  • We expect initiatives from the student and an appropriate commitment to research discussions and progress monitoring.
  • We will mainly conduct research meetings online, but we expect students to come to the AIST Waterfront (Koto-ku, Tokyo) on a regular (or long-term) basis.

What students could learn

Our goal is to guide students to develop

  • the knowledge and practice of software verification and formal mathematics
  • logical and abstract reasoning skills useful to design software systems
  • technical writing skills (in English or in Japanese) developed through the practice of research surveys and scientific presentations