Research Project Outline
We realize technologies that enable us to ensure and verify safety and reliablity of system software based on static program analysis theories, especially by type theory and model checking theory. In addition, we develop and release practical verification tools that can be widely used by system software developers.