Formal methods are a kind of methods for specification, development and verification of software/hardware, by using languages, techniques and tools based on mathematics.
Formal methods can strictly ensure the safety and reliability of software/hardware because they are supported by the validity of mathematics.
Therefore, they are often applied to the development and verification for many safety- and reliability- critical systems, e.g., control units and OSs in automobiles/airplanes/spacecrafts, air/railway traffic control systems, CPUs, cryptographic/communication protocols, medical machines.
However, core techniques of formal methods have theoretical limitations (i.e., undecidability and computational difficulty) in general.
So, we need to exercise ingenuity on reducing a real problem into solvable ones by using abstraction, approximation and relaxations, etc. and on combining multiple techniques to solve each of the reduced problems.
We tackle research on developing advanced techniques for expanding the scope of applications, and applying them to the development and verification of real products.
We try to propose/extend fundamental techniques and algorithms for specification/development/verification of systems, to expand the scope of formal methods.
We try to produce applicable formal methods by developing techniques and methods to bridge a gap between theories and practices through collaborative research with industry companies.