Information System Verification Laboratory

K. Nishizawa

Koki Nishizawa
(Associate Professor)

Office: 6-418 Ext.: 3378


03/2006, Ph.D.(Information Science and Technology), The University of Tokyo

03/2003, Master of Information Science and Technology, The University of Tokyo

Research Field

Computer Science, Logic, Algebra.

Research Overview

Formal verification of information systems and category theoretical analysis of algebraic structures.

Research Subjects

  • 1. Abstraction in model checking.
  • 2. Representation theorem of quantales.
  • 3. Stone-type duality.


Our laboratory is studying mathematical methods, such as logics, algebras, and model checking, to verify whether given information systems have no bugs.

Abstraction in model checking

We are devising mathematical methods to check that system S satisfies property P. However, if S is large-scale and complicated, a direct check cannot finish in a practical amount of time. Thus, an abstraction is necessary. An abstraction is a mathematical proof to show that all properties satisfied by simpler system T are also satisfied by S.

Stone-type duality

There is a deep relationship between algebras and spaces. For example, a Boolean algebra is an algebraic structure that satisfies the same axioms as the propositional logic. There is a one-to-one correspondence between Boolean algebras and spaces equipped with Stone topologies. Similar one-to-one correspondences are found for various spaces and algebras, called Stone-type dualities. We are searching for sufficient conditions where the extension of logics induces the extension of Stone-type dualities.

  • 1) K. Nishizawa and N. Tsumagari, "Composition of different-type relations via the Kleisli category for the continuation monad," Relational and Algebraic Methods in Computer Science, LNCS 11194, accepted (2018).
  • 2)H. Furusawa and K. Nishizawa, “Multirelational representation theorems for complete idempotent left semirings,” Journal of Logical and Algebraic Methods in Programming, vol. 84, pp. 426-439 (2015).
  • 3)K. Nishizawa and H. Furusawa, “A sufficient condition for liftable adjunctions between Eilenberg-Moore categories,” Relational and Algebraic Methods in Computer Science, LNCS 8428, pp. 261–276 (2014).
  • 4)K. Nishizawa and H. Furusawa, “Relational representation theorem for powerset quantales,” Relational and Algebraic Methods in Computer Science, LNCS 7560, pp. 207–218 (2012).
  • 5)K. Nishizawa and H. Furusawa, “Ideal completion of join semilattices over T-algebra,” Bulletin of Tottori University of Environmental Studies, vol. 9 and 10, pp. 91–103 (2012).
  • 6)K. Nishizawa, “Multi-valued modal fixed point logics for model checking,” IEICE Transactions on Information and Systems, vol. E93-D(8), pp. 2036–2039 (2010).
  • 7)K. Nishizawa, N. Tsumagari, and H. Furusawa, “The cube of Kleene algebras and the triangular prism of multirelations,” Relations and Kleene Algebra in Computer Science, LNCS 5827, pp. 276–290 (2009).
  • 8)K. Nishizawa and J. Power, “Lawvere theories enriched over a general base,” Journal of Pure and Applied Algebra, vol. 213(3), pp. 377–386 (2009).
Affiliated Academic Organizations

Japan Society for Software Science and Technology, International Society for Mathematical Sciences, The Mathematical Society of Japan

Current members
◯ Assistant Professors: 1 ◯ Undergraduates: 11