2008 |
87 | EE | Jianwen Xiang,
Dines Bjørner,
Kokichi Futatsugi:
Formal digital license language with OTS/CafeOBJ method.
AICCSA 2008: 652-660 |
86 | EE | Yasuhito Arimoto,
Michiharu Kudo,
Yuji Watanabe,
Kokichi Futatsugi:
Checking assignments of controls to risks for internal control.
ICEGOV 2008: 98-104 |
85 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes.
ICFEM 2008: 187-206 |
84 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method.
Electr. Notes Theor. Comput. Sci. 201: 127-154 (2008) |
83 | EE | Masaki Nakamura,
Weiqiang Kong,
Kazuhiro Ogata,
Kokichi Futatsugi:
A Specification Translation from Behavioral Specifications to Rewrite Specifications.
IEICE Transactions 91-D(5): 1492-1503 (2008) |
2007 |
82 | EE | Xiaoyi Chen,
Weiqiang Kong,
Kokichi Futatsugi:
Formal support for e-government system design with transparency consideration.
ICEGOV 2007: 20-29 |
81 | EE | Masaki Nakamura,
Kokichi Futatsugi:
On Equality Predicates in Algebraic Specification Languages.
ICTAC 2007: 381-395 |
80 | EE | Weiqiang Kong,
Kazuhiro Ogata,
Kokichi Futatsugi:
Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System.
IFM 2007: 393-412 |
79 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
State Machines as Inductive Types.
IEICE Transactions 90-A(12): 2985-2988 (2007) |
78 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm.
IEICE Transactions 90-A(8): 1690-1703 (2007) |
77 | EE | Weiqiang Kong,
Kazuhiro Ogata,
Kokichi Futatsugi:
Specification and Verification of Workflows with Rbac Mechanism and Sod Constraints.
International Journal of Software Engineering and Knowledge Engineering 17(1): 3-32 (2007) |
76 | EE | Masahiro Nakano,
Kazuhiro Ogata,
Masaki Nakamura,
Kokichi Futatsugi:
CrÈme: an Automatic Invariant Prover of Behavioral Specifications.
International Journal of Software Engineering and Knowledge Engineering 17(6): 783-804 (2007) |
75 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Modeling and verification of real-time systems based on equations.
Sci. Comput. Program. 66(2): 162-180 (2007) |
2006 |
74 | | Kokichi Futatsugi,
Jean-Pierre Jouannaud,
José Meseguer:
Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday
Springer 2006 |
73 | EE | Kokichi Futatsugi:
Verifying Specifications with Proof Scores in CafeOBJ.
ASE 2006: 3-10 |
72 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method.
Essays Dedicated to Joseph A. Goguen 2006: 596-615 |
71 | EE | Kazuhiro Ogata,
Masahiro Nakano,
Weiqiang Kong,
Kokichi Futatsugi:
Induction-Guided Falsification.
ICFEM 2006: 114-131 |
70 | EE | Masahiro Nakano,
Kazuhiro Ogata,
Masaki Nakamura,
Kokichi Futatsugi:
Automating Invariant Verification of Behavioral Specifications.
QSIC 2006: 49-56 |
69 | | Kazuhiro Ogata,
Weiqiang Kong,
Kokichi Futatsugi:
Falsification of OTSs by Searches of Bounded Reachable State Spaces.
SEKE 2006: 440-445 |
68 | | Jianwen Xiang,
Weiqiang Kong,
Kokichi Futatsugi,
Kazuhiro Ogata:
Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management.
WEBIST (2) 2006: 5-12 |
67 | EE | Takahiro Seino,
Kazuhiro Ogata,
Kokichi Futatsugi:
A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method.
Electr. Notes Theor. Comput. Sci. 147(1): 57-72 (2006) |
66 | EE | Masaki Nakamura,
Masahiro Watanabe,
Kokichi Futatsugi:
A Behavioral Specification of Imperative Programming Languages.
IEICE Transactions 89-A(6): 1558-1565 (2006) |
65 | EE | Hidetaka Kondoh,
Kokichi Futatsugi:
To use or not to use the goto statement: Programming styles viewed from Hoare Logic.
Sci. Comput. Program. 60(1): 82-116 (2006) |
2005 |
64 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker.
APSEC 2005: 159-166 |
63 | EE | Weiqiang Kong,
Takahiro Seino,
Kokichi Futatsugi,
Kazuhiro Ogata:
A Lightweight Integration of Theorem Proving and Model Checking for System Verification.
APSEC 2005: 59-66 |
62 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers.
CIT 2005: 937-943 |
61 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Equational Approach to Formal Analysis of TLS.
ICDCS 2005: 795-804 |
60 | EE | Kazuhiro Ogata,
Masahiro Nakano,
Masaki Nakamura,
Kokichi Futatsugi:
Chocolat/SMV: A Translator from CafeOBJ into SMV.
PDCAT 2005: 416-420 |
59 | | Weiqiang Kong,
Kazuhiro Ogata,
Kokichi Futatsugi:
Formal Analysis of Workflow Systems with Security Considerations.
SEKE 2005: 531-536 |
58 | | Kazuhiro Ogata,
Kokichi Futatsugi:
Proof Score Approach to Verification of Liveness Properties.
SEKE 2005: 608-613 |
57 | | Jittisak Senachak,
Takahiro Seino,
Kazuhiro Ogata,
Kokichi Futatsugi:
Provably Correct Translation from CafeOBJ into Java.
SEKE 2005: 614-619 |
56 | EE | Kokichi Futatsugi,
Joseph A. Goguen,
Kazuhiro Ogata:
Verifying Design with Proof Scores.
VSTTE 2005: 277-290 |
2004 |
55 | | Kokichi Futatsugi,
Fumio Mizoguchi,
Naoki Yonezaki:
Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers
Springer 2004 |
54 | EE | Takahiro Seino,
Kazuhiro Ogata,
Kokichi Futatsugi:
Supporting Case Analysis with Algebraic Specification Languages.
CIT 2004: 1073-1080 |
53 | EE | Weiqiang Kong,
Kazuhiro Ogata,
Jianwen Xiang,
Kokichi Futatsugi:
Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol.
CIT 2004: 1100-1107 |
52 | EE | Jianwen Xiang,
Kokichi Futatsugi,
Yanxiang He:
Fault Tree and Formal Methods in System Safety Analysis.
CIT 2004: 1108-1115 |
51 | | Kazuhiro Ogata,
Daigo Yamagishi,
Takahiro Seino,
Kokichi Futatsugi:
Modeling and Verification of Hybrid Systems Based on Equations.
DIPES 2004: 43-52 |
50 | | Jianwen Xiang,
Kokichi Futatsugi,
Yanxiang He:
Formal fault tree construction and system safety analysis.
IASTED Conf. on Software Engineering 2004: 378-384 |
49 | | Jianwen Xiang,
Kokichi Futatsugi,
Yanxiang He:
Formal construction model and specification of fault tree.
IASTED Conf. on Software Engineering and Applications 2004: 374-381 |
48 | | Natenapa Sriharee,
Twittie Senivongse,
Chayan Teppaboot,
Kokichi Futatsugi:
Adding Semantics to Attribute-Based Discovery of Web Services.
International Conference on Internet Computing 2004: 790-794 |
47 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
We Present a Complete Study Involving in the One Hand.
QSIC 2004: 50-59 |
2003 |
46 | EE | Toshimi Sawada,
Kouichi Kishida,
Kokichi Futatsugi:
Past, Present, and Future of SRA Implementation of CafeOBJ: Annex.
FME 2003: 7-17 |
45 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Proof Scores in the OTS/CafeOBJ Method.
FMOODS 2003: 170-184 |
44 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Formal Analysis of the NetBill Electronic Commerce Protocol.
ISSS 2003: 45-64 |
43 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Formal Verification of the Horn-Preneel Micropayment Protocol.
VMCAI 2003: 238-252 |
42 | | Razvan Diaconescu,
Kokichi Futatsugi,
Kazuhiro Ogata:
CafeOBJ: Logical Foundations and Methodologies.
Computers and Artificial Intelligence 22(3): (2003) |
41 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Flaw and modification of the iKP electronic payment protocols.
Inf. Process. Lett. 86(2): 57-62 (2003) |
2002 |
40 | EE | Chayan Tapabut,
Twittie Senivongse,
Kokichi Futatsugi:
Defining Attribute Templates for Descriptions of Distributed Services.
APSEC 2002: 425-434 |
39 | EE | Kokichi Futatsugi:
Formal Methods in CafeOBJ.
FLOPS 2002: 1-20 |
38 | | Kazuhiro Ogata,
Kokichi Futatsugi:
Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm.
FMOODS 2002: 181-195 |
37 | EE | Akira Mori,
Kokichi Futatsugi:
CafeOBJ as a Tool for Behavioral System Verification.
ISSS 2002: 461-470 |
36 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Rewriting-Based Verification of Authentication Protocols.
Electr. Notes Theor. Comput. Sci. 71: (2002) |
35 | EE | Razvan Diaconescu,
Kokichi Futatsugi:
Logical foundations of CafeOBJ.
Theor. Comput. Sci. 285(2): 289-318 (2002) |
2001 |
34 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm.
APAQS 2001: 357-366 |
33 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ.
ASE 2001: 185-192 |
32 | | Kazuhiro Ogata,
Kokichi Futatsugi:
Specifying and verifying a railroad crossing with CafeOBJ.
IPDPS 2001: 150 |
2000 |
31 | EE | Michihiro Matsumoto,
Kokichi Futatsugi:
The support tool for highly reliable component-based software development.
APSEC 2000: 172-179 |
30 | EE | Michihiro Matsumoto,
Kokichi Futatsugi:
Highly Reliable Component-Based Software Development by Using Algebraic Behavioral Specification.
ICFEM 2000: 35-44 |
29 | | Kazuhiro Ogata,
Kokichi Futatsugi:
Operational Semantics of Rewriting with the On-demand Evaluation Strategy.
SAC (2) 2000: 756-764 |
28 | EE | Kokichi Futatsugi:
Preface.
Electr. Notes Theor. Comput. Sci. 36: (2000) |
27 | EE | Razvan Diaconescu,
Kokichi Futatsugi:
Behavioural Coherence in Object-Oriented Algebraic Specification.
J. UCS 6(1): 74-96 (2000) |
1999 |
26 | EE | Michihiro Matsumoto,
Kokichi Futatsugi:
Simply Observable Behavioral Specification.
APSEC 1999: 460-467 |
25 | EE | Kazuhiro Ogata,
Kokichi Futatsugi:
Formal Verification of the MCS List-Based Queuing Lock.
ASIAN 1999: 281-293 |
24 | EE | Kazuhiro Ogata,
Shigenori Ioroi,
Kokichi Futatsugi:
Optimizing Term Rewriting Using Discrimination Nets With Specialization.
SAC 1999: 511-518 |
23 | EE | Akira Mori,
Kokichi Futatsugi:
Verifying Behavioural Specifications in CafeOBJ Environment.
World Congress on Formal Methods 1999: 1625-1643 |
22 | EE | Razvan Diaconescu,
Kokichi Futatsugi,
Shusaku Iida:
Component-Based Algebraic Specification and Verification in CafeOBJ.
World Congress on Formal Methods 1999: 1644-1663 |
1998 |
21 | EE | Kazuhiro Ogata,
Hiromichi Hirata,
Shigenori Ioroi,
Kokichi Futatsugi:
Experimental Implementation of Parallel TRAM on Massively Parallel Computer.
Euro-Par 1998: 846-851 |
20 | | Hiroshi Ishikawa,
Takuo Watanabe,
Kokichi Futatsugi,
José Meseguer,
Hideyuki Nakashima:
On the Semantics of GAEA.
Fuji International Symposium on Functional and Logic Programming 1998: 123-142 |
19 | EE | Razvan Diaconescu,
Kokichi Futatsugi:
An overview of CafeOBJ.
Electr. Notes Theor. Comput. Sci. 15: (1998) |
18 | EE | Michihiro Matsumoto,
Kokichi Futatsugi:
Test set coinduction - Toward automated verification of behavioural properties.
Electr. Notes Theor. Comput. Sci. 15: (1998) |
1997 |
17 | | Kazuhiro Ogata,
Masaru Kondo,
Shigenori Ioroi,
Kokichi Futatsugi:
Design and Implementation of Parallel TRAM.
Euro-Par 1997: 1209-1216 |
16 | | Kokichi Futatsugi,
Ataru T. Nakagawa:
An Overview of CAFE Specification Environment - An Algebraic Approach for Creating, Verifying, and Maintaining Formal Specifications over Networks.
ICFEM 1997: 170- |
15 | EE | Shin Nakajima,
Kokichi Futatsugi:
An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ.
ICSE 1997: 34-44 |
14 | | Kazuhiro Ogata,
Kokichi Futatsugi:
Implementation of Term Rewritings with the Evaluation Strategy.
PLILP 1997: 225-239 |
13 | | Kazuhiro Ogata,
Koichi Ohhara,
Kokichi Futatsugi:
TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems.
RTA 1997: 335-338 |
1996 |
12 | | Kokichi Futatsugi,
Satoshi Matsuoka:
Object Technologies for Advanced Software, Second JSSST International Symposium, ISOTAS '96, Kanazawa, Japan, March 11-15, 1996, Proceedings
Springer 1996 |
1994 |
11 | | Ataru T. Nakagawa,
Kokichi Futatsugi:
Formalizing humans in software processes.
ISPW 1994: 60-61 |
1990 |
10 | | Kazuhito Ohmaki,
Koichi Takahashi,
Kokichi Futatsugi:
A LOTOS Simulator in OBJ.
FORTE 1990: 535-538 |
9 | | Ataru T. Nakagawa,
Kokichi Futatsugi:
Software Process à la Algebra: OBJ for OBJ.
ICSE 1990: 12-23 |
8 | | Kokichi Futatsugi:
Product-centered process description = algebraic specification of environment + SCRIPT.
ISPW 1990: 95-98 |
1989 |
7 | | Ataru T. Nakagawa,
Kokichi Futatsugi:
Stepwise Refinement Process with Modularity: An Algebraic Approach.
ICSE 1989: 166-177 |
6 | | Ataru T. Nakagawa,
Kokichi Futatsugi:
Product-based process models.
ISPW 1989: 101-105 |
1988 |
5 | | Ataru T. Nakagawa,
Kokichi Futatsugi,
Satoru Tomura,
T. Shimizu:
Algebraic Specification of Macintosh's Quickdraw Using OBJ2.
ICSE 1988: 334-343 |
1987 |
4 | | Kokichi Futatsugi,
Joseph A. Goguen,
José Meseguer,
K. Okada:
Parameterized Programming in OBJ2.
ICSE 1987: 51-60 |
1985 |
3 | | Kokichi Futatsugi,
Joseph A. Goguen,
Jean-Pierre Jouannaud,
José Meseguer:
Principles of OBJ2.
POPL 1985: 52-66 |
1982 |
2 | | Kokichi Futatsugi,
Koji Okada:
A Hierarchical Structuring Method for Functional Software Systems.
ICSE 1982: 393-402 |
1980 |
1 | | Kokichi Futatsugi,
Koji Okada:
Specification Writing as Construction of Hierarchically Structured Clusters of Operators.
IFIP Congress 1980: 287-292 |