Kokichi FUTATSUGI

Formal Verification of Effectiveness of Control Activities in Business Processes
Yasuhito ARIMOTO Shusaku IIDA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2012/05/01
Vol. E95-D  No. 5  pp. 1342-1354
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Methods
Keyword: 
risk analysis, business process, formal methods, 
 Summary | Full Text:PDF
A Note on “On the Construction of Boolean Functions with Optimal Algebraic Immunity”
Yuan LI Haibin KAN Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2011/09/01
Vol. E94-A  No. 9  pp. 1877-1880
Type of Manuscript:  LETTER
Category: Cryptography and Information Security
Keyword: 
algebraic attacks, algebraic degree, algebraic immunity, Boolean functions, 
 Summary | Full Text:PDF
Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
Weiqiang KONG Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2010/05/01
Vol. E93-D  No. 5  pp. 974-984
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Specification
Keyword: 
e-Government messaging framework, formal methods, the OTS/CafeOBJ method, falsification, verification, 
 Summary | Full Text:PDF
User-Defined On-Demand Matching
Masaki NAKAMURA Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2009/07/01
Vol. E92-D  No. 7  pp. 1401-1411
Type of Manuscript:  PAPER
Category: Computation and Computational Models
Keyword: 
the evaluation strategy, lazy evaluation, on-demand matching, term rewriting, 
 Summary | Full Text:PDF
Proof Score Approach to Verification of Liveness Properties
Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2008/12/01
Vol. E91-D  No. 12  pp. 2804-2817
Type of Manuscript:  PAPER
Category: Fundamentals of Software and Theory of Programs
Keyword: 
CafeOBJ, equations, observational transition systems (OTSs), rewriting, specification, 
 Summary | Full Text:PDF
A Specification Translation from Behavioral Specifications to Rewrite Specifications
Masaki NAKAMURA Weiqiang KONG Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2008/05/01
Vol. E91-D  No. 5  pp. 1492-1503
Type of Manuscript:  PAPER
Category: Fundamentals of Software and Theory of Programs
Keyword: 
specification translation, verification, algebraic specification, behavioral specification, rewirte specification, CafeOBJ, Maude, 
 Summary | Full Text:PDF
State Machines as Inductive Types
Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2007/12/01
Vol. E90-A  No. 12  pp. 2985-2988
Type of Manuscript:  LETTER
Category: Concurrent Systems
Keyword: 
Coq, formal methods, invariant properties, program specification, observational transition systems (OTSs), 
 Summary | Full Text:PDF
Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm
Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2007/08/01
Vol. E90-A  No. 8  pp. 1690-1703
Type of Manuscript:  PAPER
Category: Concurrent Systems
Keyword: 
Maude, model checkers, k-induction, SAL, the Suzuki-Kasami algorithm, 
 Summary | Full Text:PDF
A Behavioral Specification of Imperative Programming Languages
Masaki NAKAMURA Masahiro WATANABE Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2006/06/01
Vol. E89-A  No. 6  pp. 1558-1565
Type of Manuscript:  Special Section PAPER (Special Section on Papers Selected from 2005 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC2005))
Category: 
Keyword: 
semantics of imperative programs, behavioral specification, CafeOBJ, 
 Summary | Full Text:PDF
Specification and Verification of a Single-Track Railroad Signaling in CafeOBJ
Takahiro SEINO Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2001/06/01
Vol. E84-A  No. 6  pp. 1471-1478
Type of Manuscript:  Special Section PAPER (Special Section on Papers Selected from 2000 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2000))
Category: 
Keyword: 
CafeOBJ, formal method, railroad signaling, 
 Summary | Full Text:PDF
Algebraic Approaches for Nets Using Formulas to Describe Practical Software Systems
kazuhito OHMAKI Yutaka SATO Ichiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 1993/10/25
Vol. E76-A  No. 10  pp. 1580-1590
Type of Manuscript:  Special Section PAPER (Special Section on Nets-Oriented Software Specification and Design)
Category: 
Keyword: 
Petri net, process algebra, CCS, LOTOS, user interface management system, 
 Summary | Full Text:PDF