The goal of our project is to realize technologies that enable us to ensure and verify safety and reliability 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.