Kokichi Futatsugi

ORCID

Publication Activity (10 Years)

Years Active: 1980-2022
Publications (10 Years): 14

Top Venues

Specification, Algebra, and Software

APSEC

CoRR

FASE

Publications

Kokichi Futatsugi
Advances of proof scores in CafeOBJ. Sci. Comput. Program. 224 (2022)
Kokichi Futatsugi
Advances of Proof Scores in CafeOBJ : Invited Paper. TASE (2021)
Kokichi Futatsugi
Advances of Proof Scores in CafeOBJ. CoRR (2021)
Takafumi Komoto, Kokichi Futatsugi, Nobukazu Yoshioka
A Method for Assessing the Reliability of Business Processes that Reflects Transaction Documents Checking for each Department. COMPSAC (2020)
Daniel Gaina, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
Stability of termination and sufficient-completeness under pushouts via amalgamation. Theor. Comput. Sci. 848 (2020)
Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi
A Maude environment for CafeOBJ. Formal Aspects Comput. 29 (2) (2017)
Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi
CafeInMaude: A CafeOBJ Interpreter in Maude. FASE (2016)
Takafumi Komoto, Kokichi Futatsugi, Nobukazu Yoshioka
Assessing Business Processes by Checking Transaction Documents for Inconsistency Risks and a Tool for Risk Assessment. BMSD (2016)
Masaki Nakamura, Daniel Gâinâ, Kazuhiro Ogata, Kokichi Futatsugi
Proving Sufficient Completeness of Constructor-Based Algebraic Specifications. CSA/CUTE (2015)
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates. APSEC (2015)
Hiroyuki Yoshida, Kazuhiro Ogata, Kokichi Futatsugi
Formalization and Verification of Declarative Cloud Orchestration. ICFEM (2015)
Kokichi Futatsugi
Generate & Check Method for Verifying Transition Systems in CafeOBJ. Software, Services, and Systems (2015)
Daniel Gâinâ, Kokichi Futatsugi
Initial semantics in logics with constructors. J. Log. Comput. 25 (1) (2015)
Kokichi Futatsugi
Generic Proof Scores for Generate & Check Method in CafeOBJ. Logic, Rewriting, and Concurrency (2015)
Kazuhiro Ogata, Kokichi Futatsugi
Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs. Specification, Algebra, and Software (2014)
Daniel Gâinâ, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi
On Automation of OTS/CafeOBJ Method. Specification, Algebra, and Software (2014)
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method. Specification, Algebra, and Software (2014)
Norbert Preining, Kazuhiro Ogata, Kokichi Futatsugi
Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications. LOPSTR (2014)
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications. Specification, Algebra, and Software (2014)
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
Formalization and Verification of Behavioral Correctness of Dynamic Software Updates. Electron. Notes Theor. Comput. Sci. 294 (2013)
Kazuhiro Ogata, Kokichi Futatsugi
Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method. J. Univers. Comput. Sci. 19 (6) (2013)
Hirokazu Yatsu, Takahiro Ando, Weiqiang Kong, Kenji Hisazumi, Akira Fukuda, Toshiaki Aoki, Kokichi Futatsugi
Towards Formal Description of Standards for Automotive Operating Systems. ICST Workshops (2013)
Daniel Gâinâ, Kokichi Futatsugi, Kazuhiro Ogata
Constructor-based Logics. J. Univers. Comput. Sci. 18 (16) (2012)
Kokichi Futatsugi, Daniel Gâinâ, Kazuhiro Ogata
Principles of proof scores in CafeOBJ. Theor. Comput. Sci. 464 (2012)
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms. APSEC (2012)
Yasuhito Arimoto, Shusaku Iida, Kokichi Futatsugi
Formal Verification of Effectiveness of Control Activities in Business Processes. IEICE Trans. Inf. Syst. (5) (2012)
Takafumi Komoto, Kenji Taguchi, Haralambos Mouratidis, Nobukazu Yoshioka, Kokichi Futatsugi
A Modelling Framework to Support Internal Control. SSIRI (Companion) (2011)
Yuan Li, Haibin Kan, Kokichi Futatsugi
A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity". IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (9) (2011)
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
Towards Reliable E-Government Systems with the OTS/CafeOBJ Method. IEICE Trans. Inf. Syst. (5) (2010)
Kazuhiro Ogata, Kokichi Futatsugi
Proof Score Approach to Analysis of Electronic Commerce Protocols. Int. J. Softw. Eng. Knowl. Eng. 20 (2) (2010)
Kazuhiro Ogata, Kokichi Futatsugi
A Combination of Forward and Backward Reachability Analysis Methods. ICFEM (2010)
Kokichi Futatsugi
Fostering Proof Scores in CafeOBJ. ICFEM (2010)
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications. J. Symb. Comput. 45 (5) (2010)
Tomonori Izumida, Kokichi Futatsugi, Akira Mori
A Generic Binary Analysis Method for Malware. IWSEC (2010)
Daniel Gâinâ, Kokichi Futatsugi, Kazuhiro Ogata
Constructor-Based Institutions. CALCO (2009)
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
User-Defined On-Demand Matching. IEICE Trans. Inf. Syst. (7) (2009)
Kazuhiro Ogata, Kokichi Futatsugi
Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes. ICFEM (2008)
Kazuhiro Ogata, Kokichi Futatsugi
Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method. Electron. Notes Theor. Comput. Sci. 201 (2008)
Jianwen Xiang, Dines Bjørner, Kokichi Futatsugi
Formal digital license language with OTS/CafeOBJ method. AICCSA (2008)
Kazuhiro Ogata, Kokichi Futatsugi
Proof Score Approach to Verification of Liveness Properties. IEICE Trans. Inf. Syst. (12) (2008)
Yasuhito Arimoto, Michiharu Kudo, Yuji Watanabe, Kokichi Futatsugi
Checking assignments of controls to risks for internal control. ICEGOV (2008)
Weiqiang Kong, Kazuhiro Ogata, Jian Cheng, Kokichi Futatsugi
Trace anonymity in the OTS/CafeOBJ method. CIT (2008)
Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
A Specification Translation from Behavioral Specifications to Rewrite Specifications. IEICE Trans. Inf. Syst. (5) (2008)
Masaki Nakamura, Kokichi Futatsugi
On Equality Predicates in Algebraic Specification Languages. ICTAC (2007)
Xiaoyi Chen, Weiqiang Kong, Kokichi Futatsugi
Formal support for e-government system design with transparency consideration. ICEGOV (2007)
Jianwen Xiang, Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ. Inf. Media Technol. 2 (2) (2007)
Kazuhiro Ogata, Kokichi Futatsugi
Modeling and verification of real-time systems based on equations. Sci. Comput. Program. 66 (2) (2007)
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System. IFM (2007)
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
Specification and Verification of Workflows with Rbac Mechanism and Sod Constraints. Int. J. Softw. Eng. Knowl. Eng. 17 (1) (2007)
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
CrÈme: an Automatic Invariant Prover of Behavioral Specifications. Int. J. Softw. Eng. Knowl. Eng. 17 (6) (2007)
Kazuhiro Ogata, Kokichi Futatsugi
State Machines as Inductive Types. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (12) (2007)
Kazuhiro Ogata, Kokichi Futatsugi
Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (8) (2007)
Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
Falsification of OTSs by Searches of Bounded Reachable State Spaces. SEKE (2006)
Hidetaka Kondoh, Kokichi Futatsugi
To use or not to use the goto statement: Programming styles viewed from Hoare Logic. Sci. Comput. Program. 60 (1) (2006)
Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi
Induction-Guided Falsification. ICFEM (2006)
Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer
Joseph Goguen (1941-2006). Bull. EATCS 90 (2006)
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
Automating Invariant Verification of Behavioral Specifications. QSIC (2006)
Jianwen Xiang, Weiqiang Kong, Kokichi Futatsugi, Kazuhiro Ogata
Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management. WEBIST (2) (2006)
Kokichi Futatsugi
Verifying Specifications with Proof Scores in CafeOBJ. ASE (2006)
Masaki Nakamura, Masahiro Watanabe, Kokichi Futatsugi
A Behavioral Specification of Imperative Programming Languages. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (6) (2006)
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method. Electron. Notes Theor. Comput. Sci. 147 (1) (2006)
Kazuhiro Ogata, Kokichi Futatsugi
Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method. Essays Dedicated to Joseph A. Goguen (2006)
Kazuhiro Ogata, Kokichi Futatsugi
Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers. CIT (2005)
Kazuhiro Ogata, Kokichi Futatsugi
Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker. APSEC (2005)
Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, Kokichi Futatsugi
Chocolat/SMV: A Translator from CafeOBJ into SMV. PDCAT (2005)
Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
Provably Correct Translation from CafeOBJ into Java. SEKE (2005)
Kazuhiro Ogata, Kokichi Futatsugi
Equational Approach to Formal Analysis of TLS. ICDCS (2005)
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
Mechanically supporting case analysis for verification of distributed systems. Int. J. Pervasive Comput. Commun. 1 (2) (2005)
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
Formal Analysis of Workflow Systems with Security Considerations. SEKE (2005)
Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata
A Lightweight Integration of Theorem Proving and Model Checking for System Verification. APSEC (2005)
Kazuhiro Ogata, Kokichi Futatsugi
Proof Score Approach to Verification of Liveness Properties. SEKE (2005)
Kokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogata
Verifying Design with Proof Scores. VSTTE (2005)
Natenapa Sriharee, Twittie Senivongse, Chayan Teppaboot, Kokichi Futatsugi
Adding Semantics to Attribute-Based Discovery of Web Services. International Conference on Internet Computing (2004)
Jianwen Xiang, Kokichi Futatsugi, Yanxiang He
Formal construction model and specification of fault tree. IASTED Conf. on Software Engineering and Applications (2004)
Kazuhiro Ogata, Kokichi Futatsugi
Equational Approach to Formal Verification of SET. QSIC (2004)
Jianwen Xiang, Kokichi Futatsugi, Yanxiang He
Formal fault tree construction and system safety analysis. IASTED Conf. on Software Engineering (2004)
Jianwen Xiang, Kokichi Futatsugi, Yanxiang He
Fault Tree and Formal Methods in System Safety Analysis. CIT (2004)
Kazuhiro Ogata, Daigo Yamagishi, Takahiro Seino, Kokichi Futatsugi
Modeling and Verification of Hybrid Systems Based on Equations. DIPES (2004)
Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi
Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol. CIT (2004)
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
Supporting Case Analysis with Algebraic Specification Languages. CIT (2004)
Razvan Diaconescu, Kokichi Futatsugi, Kazuhiro Ogata
CafeOBJ: Logical Foundations and Methodologies. Comput. Artif. Intell. 22 (3-4) (2003)
Kazuhiro Ogata, Kokichi Futatsugi
Flaw and modification of the iKP electronic payment protocols. Inf. Process. Lett. 86 (2) (2003)
Kazuhiro Ogata, Kokichi Futatsugi
Proof Scores in the OTS/CafeOBJ Method. FMOODS (2003)
Kazuhiro Ogata, Kokichi Futatsugi
Formal Analysis of the NetBill Electronic Commerce Protocol. ISSS (2003)
Toshimi Sawada, Kouichi Kishida, Kokichi Futatsugi
Past, Present, and Future of SRA Implementation of CafeOBJ: Annex. FME (2003)
Kazuhiro Ogata, Kokichi Futatsugi
Formal Verification of the Horn-Preneel Micropayment Protocol. VMCAI (2003)
Razvan Diaconescu, Kokichi Futatsugi
Logical foundations of CafeOBJ. Theor. Comput. Sci. 285 (2) (2002)
Kazuhiro Ogata, Kokichi Futatsugi
KP Electronic Payment Protocols. ISSS (2002)
Chayan Tapabut, Twittie Senivongse, Kokichi Futatsugi
Defining Attribute Templates for Descriptions of Distributed Services. APSEC (2002)
Kazuhiro Ogata, Kokichi Futatsugi
Rewriting-Based Verification of Authentication Protocols. Electron. Notes Theor. Comput. Sci. 71 (2002)
Kokichi Futatsugi
Formal Methods in CafeOBJ. FLOPS (2002)
Akira Mori, Kokichi Futatsugi
CafeOBJ as a Tool for Behavioral System Verification. ISSS (2002)
Kazuhiro Ogata, Kokichi Futatsugi
Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm. FMOODS (2002)
Kazuhiro Ogata, Kokichi Futatsugi
Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm. APAQS (2001)
Kazuhiro Ogata, Kokichi Futatsugi
Specifying and verifying a railroad crossing with CafeOBJ. IPDPS (2001)
Kazuhiro Ogata, Kokichi Futatsugi
Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ. ASE (2001)
Michihiro Matsumoto, Kokichi Futatsugi
Highly Reliable Component-Based Software Development by Using Algebraic Behavioral Specification. ICFEM (2000)
Michihiro Matsumoto, Kokichi Futatsugi
The support tool for highly reliable component-based software development. APSEC (2000)
Razvan Diaconescu, Kokichi Futatsugi
Behavioural Coherence in Object-Oriented Algebraic Specification. J. Univers. Comput. Sci. 6 (1) (2000)
Kazuhiro Ogata, Kokichi Futatsugi
Operational Semantics of Rewriting with the On-demand Evaluation Strategy. SAC (2) (2000)

Kokichi Futatsugi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Kokichi Futatsugi