Kokichi Futatsugi

137 papers A* 10A 2B 6C 28Misc 4Journal 33Unranked 48
YearRankTypeTitle / Venue / Authors
2025 J jnl
Proof Scores: A Survey (full version).
CoRR
Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Gaina, Duong Dinh Tran, Kokichi Futatsugi
2025 J jnl
Proof Scores: A Survey.
ACM Comput. Surv.
Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Gaina, Duong Dinh Tran, Kokichi Futatsugi
2022 J jnl
Advances of proof scores in CafeOBJ.
Sci. Comput. Program.
Kokichi Futatsugi
2021 Misc conf
Advances of Proof Scores in CafeOBJ : Invited Paper.
TASE
Kokichi Futatsugi
2021 J jnl
Advances of Proof Scores in CafeOBJ.
CoRR
Kokichi Futatsugi
2020 B conf
A Method for Assessing the Reliability of Business Processes that Reflects Transaction Documents Checking for each Department.
COMPSAC
Takafumi Komoto, Kokichi Futatsugi, Nobukazu Yoshioka
2020 J jnl
Stability of termination and sufficient-completeness under pushouts via amalgamation.
Theor. Comput. Sci.
Daniel Gaina, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
2017 J jnl
A Maude environment for CafeOBJ.
Formal Aspects Comput.
Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi
2016 — conf
Assessing Business Processes by Checking Transaction Documents for Inconsistency Risks and a Tool for Risk Assessment.
BMSD
Takafumi Komoto, Kokichi Futatsugi, Nobukazu Yoshioka
2016 B conf
CafeInMaude: A CafeOBJ Interpreter in Maude.
FASE
Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi
2015 C conf
Formalization and Verification of Declarative Cloud Orchestration.
ICFEM
Hiroyuki Yoshida, Kazuhiro Ogata, Kokichi Futatsugi
2015 — conf
Generate & Check Method for Verifying Transition Systems in CafeOBJ.
Software, Services, and Systems
Kokichi Futatsugi
2015 — conf
Generic Proof Scores for Generate & Check Method in CafeOBJ.
Logic, Rewriting, and Concurrency
Kokichi Futatsugi
2015 J jnl
Initial semantics in logics with constructors.
J. Log. Comput.
Daniel Gâinâ, Kokichi Futatsugi
2015 — conf
Proving Sufficient Completeness of Constructor-Based Algebraic Specifications.
CSA/CUTE
Masaki Nakamura, Daniel Gâinâ, Kazuhiro Ogata, Kokichi Futatsugi
2015 C conf
Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates.
APSEC
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2014 — conf
Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications.
Specification, Algebra, and Software
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
2014 C conf
Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications.
LOPSTR
Norbert Preining, Kazuhiro Ogata, Kokichi Futatsugi
2014 — conf
On Automation of OTS/CafeOBJ Method.
Specification, Algebra, and Software
Daniel Gâinâ, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi
2014 — conf
Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs.
Specification, Algebra, and Software
Kazuhiro Ogata, Kokichi Futatsugi
2014 — conf
Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method.
Specification, Algebra, and Software
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2013 J jnl
Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method.
J. Univers. Comput. Sci.
Kazuhiro Ogata, Kokichi Futatsugi
2013 — conf
Formalization and Verification of Behavioral Correctness of Dynamic Software Updates.
VSSE
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2013 — conf
Towards Formal Description of Standards for Automotive Operating Systems.
ICST Workshops
Hirokazu Yatsu, Takahiro Ando, Weiqiang Kong, Kenji Hisazumi, Akira Fukuda, Toshiaki Aoki, Kokichi Futatsugi
2012 C conf
An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms.
APSEC
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2012 J jnl
Constructor-based Logics.
J. Univers. Comput. Sci.
Daniel Gâinâ, Kokichi Futatsugi, Kazuhiro Ogata
2012 J jnl
Formal Verification of Effectiveness of Control Activities in Business Processes.
IEICE Trans. Inf. Syst.
Yasuhito Arimoto, Shusaku Iida, Kokichi Futatsugi
2012 J jnl
Principles of proof scores in CafeOBJ.
Theor. Comput. Sci.
Kokichi Futatsugi, Daniel Gâinâ, Kazuhiro Ogata
2011 — conf
A Modelling Framework to Support Internal Control.
SSIRI (Companion)
Takafumi Komoto, Kenji Taguchi, Haralambos Mouratidis, Nobukazu Yoshioka, Kokichi Futatsugi
2011 J jnl
A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity".
IEICE Trans. Fundam. Electron. Commun. Comput. Sci.
Yuan Li, Haibin Kan, Kokichi Futatsugi
2010 C conf
A Combination of Forward and Backward Reachability Analysis Methods.
ICFEM
Kazuhiro Ogata, Kokichi Futatsugi
2010 Misc conf
A Generic Binary Analysis Method for Malware.
IWSEC
Tomonori Izumida, Kokichi Futatsugi, Akira Mori
2010 C conf
Fostering Proof Scores in CafeOBJ.
ICFEM
Kokichi Futatsugi
2010 J jnl
Proof Score Approach to Analysis of Electronic Commerce Protocols.
Int. J. Softw. Eng. Knowl. Eng.
Kazuhiro Ogata, Kokichi Futatsugi
2010 J jnl
Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications.
J. Symb. Comput.
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
2010 J jnl
Towards Reliable E-Government Systems with the OTS/CafeOBJ Method.
IEICE Trans. Inf. Syst.
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2009 B conf
Constructor-Based Institutions.
CALCO
Daniel Gâinâ, Kokichi Futatsugi, Kazuhiro Ogata
2009 J jnl
User-Defined On-Demand Matching.
IEICE Trans. Inf. Syst.
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
2008 J jnl
A Specification Translation from Behavioral Specifications to Rewrite Specifications.
IEICE Trans. Inf. Syst.
Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2008 — conf
Checking assignments of controls to risks for internal control.
ICEGOV
Yasuhito Arimoto, Michiharu Kudo, Yuji Watanabe, Kokichi Futatsugi
2008 C conf
Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes.
ICFEM
Kazuhiro Ogata, Kokichi Futatsugi
2008 C conf
Formal digital license language with OTS/CafeOBJ method.
AICCSA
Jianwen Xiang, Dines Bjørner, Kokichi Futatsugi
2008 J jnl
Proof Score Approach to Verification of Liveness Properties.
IEICE Trans. Inf. Syst.
Kazuhiro Ogata, Kokichi Futatsugi
2008 C conf
Trace anonymity in the OTS/CafeOBJ method.
CIT
Weiqiang Kong, Kazuhiro Ogata, Jian Cheng, Kokichi Futatsugi
2007 B conf
Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System.
IFM
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2007 J jnl
Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm.
IEICE Trans. Fundam. Electron. Commun. Comput. Sci.
Kazuhiro Ogata, Kokichi Futatsugi
2007 J jnl
CrÈme: an Automatic Invariant Prover of Behavioral Specifications.
Int. J. Softw. Eng. Knowl. Eng.
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
2007 — conf
Formal support for e-government system design with transparency consideration.
ICEGOV
Xiaoyi Chen, Weiqiang Kong, Kokichi Futatsugi
2007 J jnl
From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ.
Inf. Media Technol.
Jianwen Xiang, Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
2007 J jnl
Modeling and verification of real-time systems based on equations.
Sci. Comput. Program.
Kazuhiro Ogata, Kokichi Futatsugi
2007 C conf
On Equality Predicates in Algebraic Specification Languages.
ICTAC
Masaki Nakamura, Kokichi Futatsugi
2007 — conf
Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method.
REFINE@IFM
Kazuhiro Ogata, Kokichi Futatsugi
2007 J jnl
Specification and Verification of Workflows with Rbac Mechanism and Sod Constraints.
Int. J. Softw. Eng. Knowl. Eng.
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2007 J jnl
State Machines as Inductive Types.
IEICE Trans. Fundam. Electron. Commun. Comput. Sci.
Kazuhiro Ogata, Kokichi Futatsugi
2006 J jnl
A Behavioral Specification of Imperative Programming Languages.
IEICE Trans. Fundam. Electron. Commun. Comput. Sci.
Masaki Nakamura, Masahiro Watanabe, Kokichi Futatsugi
2006 — ed.
Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday
Essays Dedicated to Joseph A. Goguen
Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer
2006 — conf
Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management.
WEBIST (2)
Jianwen Xiang, Weiqiang Kong, Kokichi Futatsugi, Kazuhiro Ogata
2006 — conf
Automating Invariant Verification of Behavioral Specifications.
QSIC
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
2006 C conf
Falsification of OTSs by Searches of Bounded Reachable State Spaces.
SEKE
Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
2006 C conf
Induction-Guided Falsification.
ICFEM
Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi
2006 J jnl
Joseph Goguen (1941-2006).
Bull. EATCS
Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer
2006 — conf
Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method.
Essays Dedicated to Joseph A. Goguen
Kazuhiro Ogata, Kokichi Futatsugi
2006 J jnl
To use or not to use the goto statement: Programming styles viewed from Hoare Logic.
Sci. Comput. Program.
Hidetaka Kondoh, Kokichi Futatsugi
2006 A* conf
Verifying Specifications with Proof Scores in CafeOBJ.
ASE
Kokichi Futatsugi
2005 C conf
A Lightweight Integration of Theorem Proving and Model Checking for System Verification.
APSEC
Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata
2005 — conf
A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method.
RULE@RDP
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2005 C conf
Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers.
CIT
Kazuhiro Ogata, Kokichi Futatsugi
2005 C conf
Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker.
APSEC
Kazuhiro Ogata, Kokichi Futatsugi
2005 C conf
Chocolat/SMV: A Translator from CafeOBJ into SMV.
PDCAT
Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, Kokichi Futatsugi
2005 A conf
Equational Approach to Formal Analysis of TLS.
ICDCS
Kazuhiro Ogata, Kokichi Futatsugi
2005 C conf
Formal Analysis of Workflow Systems with Security Considerations.
SEKE
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2005 J jnl
Mechanically supporting case analysis for verification of distributed systems.
Int. J. Pervasive Comput. Commun.
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2005 C conf
Proof Score Approach to Verification of Liveness Properties.
SEKE
Kazuhiro Ogata, Kokichi Futatsugi
2005 C conf
Provably Correct Translation from CafeOBJ into Java.
SEKE
Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2005 — conf
Verifying Design with Proof Scores.
VSTTE
Kokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogata
2004 — conf
Adding Semantics to Attribute-Based Discovery of Web Services.
International Conference on Internet Computing
Natenapa Sriharee, Twittie Senivongse, Chayan Teppaboot, Kokichi Futatsugi
2004 — conf
Equational Approach to Formal Verification of SET.
QSIC
Kazuhiro Ogata, Kokichi Futatsugi
2004 C conf
Fault Tree and Formal Methods in System Safety Analysis.
CIT
Jianwen Xiang, Kokichi Futatsugi, Yanxiang He
2004 C conf
Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol.
CIT
Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi
2004 — conf
Formal construction model and specification of fault tree.
IASTED Conf. on Software Engineering and Applications
Jianwen Xiang, Kokichi Futatsugi, Yanxiang He
2004 — conf
Formal fault tree construction and system safety analysis.
IASTED Conf. on Software Engineering
Jianwen Xiang, Kokichi Futatsugi, Yanxiang He
2004 — conf
Modeling and Verification of Hybrid Systems Based on Equations.
DIPES
Kazuhiro Ogata, Daigo Yamagishi, Takahiro Seino, Kokichi Futatsugi
2004 — ed.
Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers
ISSS
Kokichi Futatsugi, Fumio Mizoguchi, Naoki Yonezaki
2004 C conf
Supporting Case Analysis with Algebraic Specification Languages.
CIT
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2003 J jnl
CafeOBJ: Logical Foundations and Methodologies.
Comput. Artif. Intell.
Razvan Diaconescu, Kokichi Futatsugi, Kazuhiro Ogata
2003 J jnl
Flaw and modification of the iKP electronic payment protocols.
Inf. Process. Lett.
Kazuhiro Ogata, Kokichi Futatsugi
2003 — conf
Formal Analysis of the NetBill Electronic Commerce Protocol.
ISSS
Kazuhiro Ogata, Kokichi Futatsugi
2003 B conf
Formal Verification of the Horn-Preneel Micropayment Protocol.
VMCAI
Kazuhiro Ogata, Kokichi Futatsugi
2003 — conf
Past, Present, and Future of SRA Implementation of CafeOBJ: Annex.
FME
Toshimi Sawada, Kouichi Kishida, Kokichi Futatsugi
2003 — conf
Proof Scores in the OTS/CafeOBJ Method.
FMOODS
Kazuhiro Ogata, Kokichi Futatsugi
2002 — conf
CafeOBJ as a Tool for Behavioral System Verification.
ISSS
Akira Mori, Kokichi Futatsugi
2002 C conf
Defining Attribute Templates for Descriptions of Distributed Services.
APSEC
Chayan Tapabut, Twittie Senivongse, Kokichi Futatsugi
2002 — conf
Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm.
FMOODS
Kazuhiro Ogata, Kokichi Futatsugi
2002 — conf
Formal Analysis of the
ISSS
Kazuhiro Ogata, Kokichi Futatsugi
2002 Misc conf
Formal Methods in CafeOBJ.
FLOPS
Kokichi Futatsugi
2002 J jnl
Logical foundations of CafeOBJ.
Theor. Comput. Sci.
Razvan Diaconescu, Kokichi Futatsugi
2002 — conf
Rewriting-Based Verification of Authentication Protocols.
WRLA
Kazuhiro Ogata, Kokichi Futatsugi
2001 — conf
Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm.
APAQS
Kazuhiro Ogata, Kokichi Futatsugi
2001 A* conf
Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ.
ASE
Kazuhiro Ogata, Kokichi Futatsugi
2001 A conf
Specifying and verifying a railroad crossing with CafeOBJ.
IPDPS
Kazuhiro Ogata, Kokichi Futatsugi
2000 J jnl
Behavioural Coherence in Object-Oriented Algebraic Specification.
J. Univers. Comput. Sci.
Razvan Diaconescu, Kokichi Futatsugi
2000 C conf
Highly Reliable Component-Based Software Development by Using Algebraic Behavioral Specification.
ICFEM
Michihiro Matsumoto, Kokichi Futatsugi
2000 — conf
Operational Semantics of Rewriting with the On-demand Evaluation Strategy.
SAC (2)
Kazuhiro Ogata, Kokichi Futatsugi
2000 — conf
Preface.
WRLA
Kokichi Futatsugi
2000 — ed.
The 3rd International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanzawa, Japan, September 18-20, 2000
WRLA
Kokichi Futatsugi
2000 C conf
The support tool for highly reliable component-based software development.
APSEC
Michihiro Matsumoto, Kokichi Futatsugi
1999 — conf
Component-Based Algebraic Specification and Verification in CafeOBJ.
World Congress on Formal Methods
Razvan Diaconescu, Kokichi Futatsugi, Shusaku Iida
1999 — ch.
Component-Based Algebraic Specification.
Behavioral Specifications of Businesses and Systems
Shusaku Iida, Kokichi Futatsugi, Razvan Diaconescu
1999 — conf
Formal Verification of the MCS List-Based Queuing Lock.
ASIAN
Kazuhiro Ogata, Kokichi Futatsugi
1999 Misc conf
Optimizing Term Rewriting Using Discrimination Nets With Specialization.
SAC
Kazuhiro Ogata, Shigenori Ioroi, Kokichi Futatsugi
1999 C conf
Simply Observable Behavioral Specification.
APSEC
Michihiro Matsumoto, Kokichi Futatsugi
1999 — conf
Verifying Behavioural Specifications in CafeOBJ Environment.
World Congress on Formal Methods
Akira Mori, Kokichi Futatsugi
1998 — conf
An overview of CafeOBJ.
WRLA
Razvan Diaconescu, Kokichi Futatsugi
1998 — book
Cafeobj Report - The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification
Razvan Diaconescu, Kokichi Futatsugi
1998 — conf
Experimental Implementation of Parallel TRAM on Massively Parallel Computer.
Euro-Par
Kazuhiro Ogata, Hiromichi Hirata, Shigenori Ioroi, Kokichi Futatsugi
1998 A* ed.
Forging New Links, Proceedings of the 1998 International Conference on Software Engineering, ICSE 98, Kyoto, Japan, April 19-25, 1998.
ICSE
Koji Torii, Kokichi Futatsugi, Richard A. Kemmerer
1998 — conf
On the Semantics of GAEA.
Fuji International Symposium on Functional and Logic Programming
Hiroshi Ishikawa, Takuo Watanabe, Kokichi Futatsugi, José Meseguer, Hideyuki Nakashima
1998 — conf
Test set coinduction - Toward automated verification of behavioural properties.
WRLA
Michihiro Matsumoto, Kokichi Futatsugi
1997 A* conf
An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ.
ICSE
Shin Nakajima, Kokichi Futatsugi
1997 C conf
An Overview of CAFE Specification Environment - An Algebraic Approach for Creating, Verifying, and Maintaining Formal Specifications over Networks.
ICFEM
Kokichi Futatsugi, Ataru T. Nakagawa
1997 — conf
Design and Implementation of Parallel TRAM.
Euro-Par
Kazuhiro Ogata, Masaru Kondo, Shigenori Ioroi, Kokichi Futatsugi
1997 — conf
Implementation of Term Rewritings with the Evaluation Strategy.
PLILP
Kazuhiro Ogata, Kokichi Futatsugi
1997 — conf
TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems.
RTA
Kazuhiro Ogata, Koichi Ohhara, Kokichi Futatsugi
1996 — ed.
Object Technologies for Advanced Software, Second JSSST International Symposium, ISOTAS '96, Kanazawa, Japan, March 11-15, 1996, Proceedings
ISOTAS
Kokichi Futatsugi, Satoshi Matsuoka
1994 — conf
Formalizing humans in software processes.
ISPW
Ataru T. Nakagawa, Kokichi Futatsugi
1991 J jnl
Propagating changes in algebraic specifications.
Softw. Eng. J.
Ataru T. Nakagawa, Kokichi Futatsugi
1991 B conf
Specifications of a general user interface in LOTOS and OBJ.
COMPSAC
Deddo Wiersma, Kazuhito Ohmaki, Kokichi Futatsugi
1990 C conf
A LOTOS Simulator in OBJ.
FORTE
Kazuhito Ohmaki, Koichi Takahashi, Kokichi Futatsugi
1990 — conf
Product-centered process description = algebraic specification of environment + SCRIPT.
ISPW
Kokichi Futatsugi
1990 A* conf
Software Process à la Algebra: OBJ for OBJ.
ICSE
Ataru T. Nakagawa, Kokichi Futatsugi
1989 — conf
Product-based process models.
ISPW
Ataru T. Nakagawa, Kokichi Futatsugi
1989 A* conf
Stepwise Refinement Process with Modularity: An Algebraic Approach.
ICSE
Ataru T. Nakagawa, Kokichi Futatsugi
1988 A* conf
Algebraic Specification of Macintosh's Quickdraw Using OBJ2.
ICSE
Ataru T. Nakagawa, Kokichi Futatsugi, Satoru Tomura, T. Shimizu
1987 A* conf
Parameterized Programming in OBJ2.
ICSE
Kokichi Futatsugi, Joseph A. Goguen, José Meseguer, Koji Okada
1985 A* conf
Principles of OBJ2.
POPL
Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, José Meseguer
1982 A* conf
A Hierarchical Structuring Method for Functional Software Systems.
ICSE
Kokichi Futatsugi, Koji Okada
1980 — conf
Specification Writing as Construction of Hierarchically Structured Clusters of Operators.
IFIP Congress
Kokichi Futatsugi, Koji Okada