
kb.is.s.u-tokyo.ac.jp
Kobayashi LaboratoryDept of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo. Recent research topics include:. This is an extension of traditional model checking that has been successfully applied to system verification. We have recently constructed the first higher-order model checker in the world. By applying the higher-order model checking mentioned above, we are developing fully-automated program verification tools for programming languages like ML and Java. Tomohiro Kaizu...
http://kb.is.s.u-tokyo.ac.jp/