TOP Page >  Profile

情報研究棟IS Building II 9F
To Lab's Site


Full text / JAIST Repository



Kokichi Futatsugi Research Professor
School of Information Science、Intelligent Robotics Area


B.E., M.E.and Ph.D. from Tohoku University (1970,1972,1975)

■Professional Career

ETL (Electrotechnical Lab), MITI, Japanese Government (1975-1992), International Fellow at SRI International, Calf., USA (1983-1984),


Formal Methods, Formal Specification Languages, Systems Verification, System Security and Safety, Concurrent and Cooperative systems, Software Engineering

■Research Keywords

formal methods, specification/design language, systems verification, software engineering



  • CAFE: An Industiral-Strength Algebraic Formal Method,Kokichi Futatsugi, Aataru Nakagawa, Tetsuo Tamai, editors,Elsevier,2000,xiv+194 pages

◇Published Papers

  • Liveness properties in CafeOBJ ?a case study for meta-level specifications,Norbert Preining, Kazuhiro Ogata, and Kokichi Futatsugi,Logic-Based Program Synthesis and Transformation ?24th International Symposium, LOPSTR 2014Lecture Notes in Computer ScienceSpringer,8981,182, 12,2015/03
  • Automating Invariant Verification of Behavioral Specifications,Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, and Kokichi Futatsugi ,In Proceedings of The Sixth IEEE International Conference on Quality Software (QSIC2006),pp. 49-56,Oct. 2006
  • A Behavioral Specification of Imperative Programming Languages,Nakamura, M., Watanabe, M., Futatsugi, K.,IEICE Transactions on Fundamentals of Electronics, Communications ancComputer Sciences,Vol. E89-A,No. 6,pp. 1558-1565,JUNE 2006

Display All

◇Lectures and Presentations

  • Provably Correct Translation from OTS/CafeOBJ Specifications to Java Programs,Jitticak Senachak, Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi,情報科学技術フォーラム FIT2004 一般講演論文集第1分冊,4-Sep
  • Verifications with Proof Scores in CafeOBJ,Kokichi Futatsugi, Joseph A. Goguen, and Kazuhiro Ogata,17th Int. Workshop on Algebraic Development Techniques,Barcelona, Spain,27th-29th March 2004
  • Formal analysis of the NetBill electronic commerce protocol,Kazuhiro Ogata and Kokichi Futatsugi,Proc. of the Second International Symposium on Software Security (ISSS2003),Tokyo Institute of Technology, Oookayama, Tokyo,4th-6th November 2003

Display All

■Extramural Activities

◇Other Activities

  • 9TH INTERNATIONAL WORKSHOP ONREWRITING LOGIC AND ITS APPLICATIONS (WRLA 2012),Member, Steering CommitteeMember, Program Committee,2012/03/24 - 2012/03/25
  • The 4th International Conference on Theory and Practice of Electronic Governance (ICEGOV2010),program committee member,2010/10/25 - 2010/10/28
  • 32th International Conference on Software Engineering (ICSE 2010), New Ideas and Emerging Results Track,program committee member,2010/05/02 - 2010/05/08

Display All