Kokichi Futatsugi

Sci. Comput. Program., 2022

2021

Advances of Proof Scores in CafeOBJ : Invited Paper.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Theoretical Aspects of Software Engineering, 2021

2020

Stability of termination and sufficient-completeness under pushouts via amalgamation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2020

A Method for Assessing the Reliability of Business Processes that Reflects Transaction Documents Checking for each Department.

[BibT_eX]

[DOI]

Takafumi Komoto

Nobukazu Yoshioka

Proceedings of the 44th IEEE Annual Computers, Software, and Applications Conference, 2020

2017

A Maude environment for CafeOBJ.

[BibT_eX]

[DOI]

Adrián Riesco

Formal Aspects Comput., 2017

2016

CafeInMaude: A CafeOBJ Interpreter in Maude.

[BibT_eX]

[DOI]

Adrián Riesco

Proceedings of the Fundamental Approaches to Software Engineering, 2016

Assessing Business Processes by Checking Transaction Documents for Inconsistency Risks and a Tool for Risk Assessment.

[BibT_eX]

[DOI]

Takafumi Komoto

Nobukazu Yoshioka

Proceedings of the Business Modeling and Software Design - 6th International Symposium, 2016

2015

Initial semantics in logics with constructors.

[BibT_eX]

[DOI]

J. Log. Comput., 2015

Formalization and Verification of Declarative Cloud Orchestration.

[BibT_eX]

[DOI]

Hiroyuki Yoshida

Proceedings of the Formal Methods and Software Engineering, 2015

Proving Sufficient Completeness of Constructor-Based Algebraic Specifications.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computer Science and Ubiquitous Computing, 2015

Generic Proof Scores for Generate & Check Method in CafeOBJ.

[BibT_eX]

[DOI]

Proceedings of the Logic, Rewriting, and Concurrency, 2015

Generate & Check Method for Verifying Transition Systems in CafeOBJ.

[BibT_eX]

[DOI]

Proceedings of the Software, 2015

Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates.

[BibT_eX]

[DOI]

Proceedings of the 2015 Asia-Pacific Software Engineering Conference, 2015

2014

Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications.

[BibT_eX]

[DOI]

Norbert Preining

Proceedings of the Logic-Based Program Synthesis and Transformation, 2014

Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs.

[BibT_eX]

[DOI]

Proceedings of the Specification, Algebra, and Software, 2014

Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications.

[BibT_eX]

[DOI]

Proceedings of the Specification, Algebra, and Software, 2014

On Automation of OTS/CafeOBJ Method.

[BibT_eX]

[DOI]

Proceedings of the Specification, Algebra, and Software, 2014

Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method.

[BibT_eX]

[DOI]

Proceedings of the Specification, Algebra, and Software, 2014

2013

Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2013

Formalization and Verification of Behavioral Correctness of Dynamic Software Updates.

[BibT_eX]

[DOI]

Proceedings of the 2013 Validation Strategies for Software Evolution Workshop, 2013

Towards Formal Description of Standards for Automotive Operating Systems.

[BibT_eX]

[DOI]

Proceedings of the Sixth IEEE International Conference on Software Testing, 2013

2012

Principles of proof scores in CafeOBJ.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2012

Constructor-based Logics.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2012

Formal Verification of Effectiveness of Control Activities in Business Processes.

[BibT_eX]

[DOI]

Yasuhito Arimoto

Shusaku Iida

IEICE Trans. Inf. Syst., 2012

An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms.

[BibT_eX]

[DOI]

Proceedings of the 19th Asia-Pacific Software Engineering Conference, 2012

2011

A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity".

[BibT_eX]

[DOI]

Yuan Li

Haibin Kan

IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2011

A Modelling Framework to Support Internal Control.

[BibT_eX]

[DOI]

Takafumi Komoto

Kenji Taguchi

Haralambos Mouratidis

Nobukazu Yoshioka

Proceedings of the Fifth International Conference on Secure Software Integration and Reliability Improvement, 2011

2010

Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications.

[BibT_eX]

[DOI]

J. Symb. Comput., 2010

Proof Score Approach to Analysis of Electronic Commerce Protocols.

[BibT_eX]

[DOI]

Int. J. Softw. Eng. Knowl. Eng., 2010

Towards Reliable E-Government Systems with the OTS/CafeOBJ Method.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2010

A Generic Binary Analysis Method for Malware.

[BibT_eX]

[DOI]

Tomonori Izumida

Akira Mori

Proceedings of the Advances in Information and Computer Security, 2010

A Combination of Forward and Backward Reachability Analysis Methods.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2010

Fostering Proof Scores in CafeOBJ.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2010

2009

User-Defined On-Demand Matching.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2009

Constructor-Based Institutions.

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2009

2008

Proof Score Approach to Verification of Liveness Properties.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2008

A Specification Translation from Behavioral Specifications to Rewrite Specifications.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2008

Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2008

Checking assignments of controls to risks for internal control.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Theory and Practice of Electronic Governance, 2008

Formal digital license language with OTS/CafeOBJ method.

[BibT_eX]

[DOI]

Dines Bjørner

Proceedings of the 6th ACS/IEEE International Conference on Computer Systems and Applications, 2008

Trace anonymity in the OTS/CafeOBJ method.

[BibT_eX]

[DOI]

Proceedings of 8th IEEE International Conference on Computer and Information Technology, 2008

2007

Modeling and verification of real-time systems based on equations.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2007

From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ.

[BibT_eX]

[DOI]

Inf. Media Technol., 2007

CrÈme: an Automatic Invariant Prover of Behavioral Specifications.

[BibT_eX]

[DOI]

Int. J. Softw. Eng. Knowl. Eng., 2007

Specification and Verification of Workflows with Rbac Mechanism and Sod Constraints.

[BibT_eX]

[DOI]

Int. J. Softw. Eng. Knowl. Eng., 2007

State Machines as Inductive Types.

[BibT_eX]

[DOI]

IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2007

Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm.

[BibT_eX]

[DOI]

IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2007

Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method.

[BibT_eX]

[DOI]

Proceedings of the BCS-FACS Refinement Workshop, 2007

Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

On Equality Predicates in Algebraic Specification Languages.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2007

Formal support for e-government system design with transparency consideration.

[BibT_eX]

[DOI]

Xiaoyi Chen

Proceedings of the 1st International Conference on Theory and Practice of Electronic Governance, 2007

2006

To use or not to use the goto statement: Programming styles viewed from Hoare Logic.

[BibT_eX]

[DOI]

Hidetaka Kondoh

Sci. Comput. Program., 2006

A Behavioral Specification of Imperative Programming Languages.

[BibT_eX]

[DOI]

Masahiro Watanabe

IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2006

Joseph Goguen (1941-2006).

[BibT_eX]

Jean-Pierre Jouannaud

José Meseguer

Bull. EATCS, 2006

Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management.

[BibT_eX]

Proceedings of the WEBIST 2006, 2006

Falsification of OTSs by Searches of Bounded Reachable State Spaces.

[BibT_eX]

Proceedings of the Eighteenth International Conference on Software Engineering & Knowledge Engineering (SEKE'2006), 2006

Automating Invariant Verification of Behavioral Specifications.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Conference on Quality Software (QSIC 2006), 2006

Verifying Specifications with Proof Scores in CafeOBJ.

[BibT_eX]

[DOI]

Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), 2006

Induction-Guided Falsification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2006

Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method.

[BibT_eX]

[DOI]

Proceedings of the Algebra, Meaning, and Computation, 2006

2005

Mechanically supporting case analysis for verification of distributed systems.

[BibT_eX]

[DOI]

Takahiro Seino

Int. J. Pervasive Comput. Commun., 2005

A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method.

[BibT_eX]

[DOI]

Takahiro Seino

Proceedings of the 6th International Workshop on Rule-Based Programming, 2005

Verifying Design with Proof Scores.

[BibT_eX]

[DOI]

Joseph A. Goguen

Proceedings of the Verified Software: Theories, 2005

Provably Correct Translation from CafeOBJ into Java.

[BibT_eX]

Proceedings of the 17th International Conference on Software Engineering and Knowledge Engineering (SEKE'2005), 2005

Formal Analysis of Workflow Systems with Security Considerations.

[BibT_eX]

Proceedings of the 17th International Conference on Software Engineering and Knowledge Engineering (SEKE'2005), 2005

Chocolat/SMV: A Translator from CafeOBJ into SMV.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Conference on Parallel and Distributed Computing, 2005

Equational Approach to Formal Analysis of TLS.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Distributed Computing Systems (ICDCS 2005), 2005

Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker.

[BibT_eX]

[DOI]

Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 2005

A Lightweight Integration of Theorem Proving and Model Checking for System Verification.

[BibT_eX]

[DOI]

Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 2005

Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on Computer and Information Technology (CIT 2005), 2005

2004

Equational Approach to Formal Verification of SET.

[BibT_eX]

[DOI]

Proceedings of the 4th International Conference on Quality Software (QSIC 2004), 2004

Modeling and Verification of Hybrid Systems Based on Equations.

[BibT_eX]

[DOI]

Proceedings of the Design Methods and Applications for Distributed Embedded Systems, 2004

Adding Semantics to Attribute-Based Discovery of Web Services.

[BibT_eX]

Proceedings of the International Conference on Internet Computing, 2004

Formal construction model and specification of fault tree.

[BibT_eX]

Yanxiang He

Proceedings of the IASTED Conference on Software Engineering and Applications, 2004

Formal fault tree construction and system safety analysis.

[BibT_eX]

Yanxiang He

Proceedings of the IASTED International Conference on Software Engineering, 2004

Fault Tree and Formal Methods in System Safety Analysis.

[BibT_eX]

[DOI]

Yanxiang He

Proceedings of the 2004 International Conference on Computer and Information Technology (CIT 2004), 2004

Supporting Case Analysis with Algebraic Specification Languages.

[BibT_eX]

[DOI]

Takahiro Seino

Proceedings of the 2004 International Conference on Computer and Information Technology (CIT 2004), 2004

Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol.

[BibT_eX]

[DOI]

Proceedings of the 2004 International Conference on Computer and Information Technology (CIT 2004), 2004

2003

Flaw and modification of the iKP electronic payment protocols.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2003

CafeOBJ: Logical Foundations and Methodologies.

[BibT_eX]

[DOI]

Comput. Artif. Intell., 2003

Formal Verification of the Horn-Preneel Micropayment Protocol.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2003

Formal Analysis of the NetBill Electronic Commerce Protocol.

[BibT_eX]

[DOI]

Proceedings of the Software Security, 2003

Proof Scores in the OTS/CafeOBJ Method.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2003

Past, Present, and Future of SRA Implementation of CafeOBJ: Annex.

[BibT_eX]

[DOI]

Toshimi Sawada

Kouichi Kishida

Proceedings of the FME 2003: Formal Methods, 2003

2002

Logical foundations of CafeOBJ.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2002

Rewriting-Based Verification of Authentication Protocols.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Workshop on Rewriting logic and Its Applications, 2002

CafeOBJ as a Tool for Behavioral System Verification.

[BibT_eX]

[DOI]

Akira Mori

Proceedings of the Software Security -- Theories and Systems, 2002

Formal Analysis of the <i>i</i>KP Electronic Payment Protocols.

[BibT_eX]

[DOI]

Proceedings of the Software Security -- Theories and Systems, 2002

Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm.

[BibT_eX]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems V, 2002

Formal Methods in CafeOBJ.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 6th International Symposium, 2002

Defining Attribute Templates for Descriptions of Distributed Services.

[BibT_eX]

[DOI]

Chayan Tapabut

Twittie Senivongse

Proceedings of the 9th Asia-Pacific Software Engineering Conference (APSEC 2002), 2002

2001

Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001

Specifying and verifying a railroad crossing with CafeOBJ.

[BibT_eX]

[DOI]

Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01), 2001

Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm.

[BibT_eX]

[DOI]

Proceedings of the 2nd Asia-Pacific Conference on Quality Software (APAQS 2001), 2001

2000

Behavioural Coherence in Object-Oriented Algebraic Specification.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2000

Preface.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, 2000

Operational Semantics of Rewriting with the On-demand Evaluation Strategy.

[BibT_eX]

[DOI]

Proceedings of the Applied Computing 2000, 2000

Highly Reliable Component-Based Software Development by Using Algebraic Behavioral Specification.

[BibT_eX]

[DOI]

Proceedings of the 3rd IEEE International Conference on Formal Engineering Methods, 2000

The support tool for highly reliable component-based software development.

[BibT_eX]

[DOI]

Proceedings of the 7th Asia-Pacific Software Engineering Conference (APSEC 2000), 2000

1999

Optimizing Term Rewriting Using Discrimination Nets With Specialization.

[BibT_eX]

[DOI]

Shigenori Ioroi

Proceedings of the 1999 ACM Symposium on Applied Computing, 1999

Verifying Behavioural Specifications in CafeOBJ Environment.

[BibT_eX]

[DOI]

Akira Mori

Proceedings of the FM'99 - Formal Methods, 1999

Component-Based Algebraic Specification and Verification in CafeOBJ.

[BibT_eX]

[DOI]

Shusaku Iida

Proceedings of the FM'99 - Formal Methods, 1999

Formal Verification of the MCS List-Based Queuing Lock.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computing Science, 1999

Simply Observable Behavioral Specification.

[BibT_eX]

[DOI]

Proceedings of the 6th Asia-Pacific Software Engineering Conference (APSEC '99), 1999

Component-Based Algebraic Specification.

[BibT_eX]

[DOI]

Shusaku Iida

Proceedings of the Behavioral Specifications of Businesses and Systems, 1999

1998

Cafeobj Report - The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification

[BibT_eX]

[DOI]

AMAST Series in Computing 6, World Scientific, ISBN: 978-981-4518-23-9, 1998

Test set coinduction - Toward automated verification of behavioural properties.

[BibT_eX]

[DOI]

Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

An overview of CafeOBJ.

[BibT_eX]

[DOI]

Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

On the Semantics of GAEA.

[BibT_eX]

Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, 1998

Experimental Implementation of Parallel TRAM on Massively Parallel Computer.

[BibT_eX]

[DOI]

Proceedings of the Euro-Par '98 Parallel Processing, 1998

1997

TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems.

[BibT_eX]

[DOI]

Koichi Ohhara

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

Implementation of Term Rewritings with the Evaluation Strategy.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages: Implementations, 1997

An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ.

[BibT_eX]

[DOI]

Shin Nakajima

Proceedings of the Pulling Together, 1997

An Overview of CAFE Specification Environment - An Algebraic Approach for Creating, Verifying, and Maintaining Formal Specifications over Networks.

[BibT_eX]

[DOI]

Proceedings of the First IEEE International Conference on Formal Engineering Methods, 1997

Design and Implementation of Parallel TRAM.

[BibT_eX]

[DOI]

Proceedings of the Euro-Par '97 Parallel Processing, 1997

1994

Formalizing humans in software processes.

[BibT_eX]

[DOI]

Proceedings of the Ninth International Software Process Workshop (ISPW '94), 1994

1991

Propagating changes in algebraic specifications.

[BibT_eX]

[DOI]

Softw. Eng. J., 1991

Specifications of a general user interface in LOTOS and OBJ.

[BibT_eX]

[DOI]

Deddo Wiersma

Kazuhito Ohmaki

Proceedings of the Fifteenth Annual International Computer Software and Applications Conference, 1991

1990

Product-centered process description = algebraic specification of environment + SCRIPT.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Software Process Workshop (ISPW '90), 1990

Software Process à la Algebra: OBJ for OBJ.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Software Engineering, 1990

A LOTOS Simulator in OBJ.

[BibT_eX]

Kazuhito Ohmaki

Koichi Takahashi

Proceedings of the Formal Description Techniques, 1990

1989

Product-based process models.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Software Process Workshop (ISPW '89), 1989

Stepwise Refinement Process with Modularity: An Algebraic Approach.

[BibT_eX]

[DOI]

Proceedings of the 11th International Conference on Software Engineering, 1989

1988

Algebraic Specification of Macintosh's Quickdraw Using OBJ2.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1988

1987

Parameterized Programming in OBJ2.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 9th International Conference on Software Engineering, Monterey, California, USA, March 30, 1987

1985

Principles of OBJ2.

[BibT_eX]

[DOI]

Joseph A. Goguen

Jean-Pierre Jouannaud

José Meseguer

Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985

1982

A Hierarchical Structuring Method for Functional Software Systems.

[BibT_eX]

[DOI]

Koji Okada

Proceedings of the Proceedings, 1982

1980

Specification Writing as Construction of Hierarchically Structured Clusters of Operators.

[BibT_eX]