Travelled to:1 × Italy
1 × Republic of China
1 × Singapore
1 × Spain
2 × France
3 × Japan
3 × United Kingdom
7 × USA
Collaborated with:K.Ogata R.Diaconescu A.T.Nakagawa W.Kong ∅ K.Okada J.Meseguer A.Mori M.Matsumoto S.Nakajima J.A.Goguen N.Preining T.Sawada K.Kishida S.Iida S.Ioroi K.Ohhara A.R.0001 K.O.0001 J.Senachak T.Seino S.Tomura T.Shimizu J.Jouannaud H.Ishikawa T.Watanabe H.Nakashima
Talks about:obj (17) cafe (13) algebra (6) specif (6) verif (6) system (5) rewrit (5) formal (4) properti (3) approach (3)
Person: Kokichi Futatsugi
DBLP: Futatsugi:Kokichi
Facilitated 2 volumes:
Ed
EdContributed to:
2014
2007
2006
20062005
2003
2003
200220022001
200019991999199819981997
1997
199720021990198919881987
19851982
2016Wrote 30 papers:
- LOPSTR-2014-PreiningOF #case study #liveness #specification
- Liveness Properties in CafeOBJ — A Case Study for Meta-Level Specifications (NP, KO, KF), pp. 182–198.
- IFM-2007-KongOF #algebra #analysis #formal method
- Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System (WK, KO, KF), pp. 393–412.
- ASE-2006-Futatsugi #proving #specification #verification
- Verifying Specifications with Proof Scores in CafeOBJ (KF), pp. 3–10.
- SEKE-2006-OgataKF #bound
- Falsification of OTSs by Searches of Bounded Reachable State Spaces (KO, WK, KF), pp. 440–445.
- SEKE-2005-KongOF #analysis #formal method #security #workflow
- Formal Analysis of Workflow Systems with Security Considerations (WK, KO, KF), pp. 531–536.
- SEKE-2005-OgataF #approach #liveness #proving #verification
- Proof Score Approach to Verification of Liveness Properties (KO, KF), pp. 608–613.
- SEKE-2005-SenachakSOF #java
- Provably Correct Translation from CafeOBJ into Java (JS, TS, KO, KF), pp. 614–619.
- FME-2003-SawadaKF #future of #implementation #past present future
- Past, Present, and Future of SRA Implementation of CafeOBJ: Annex (TS, KK, KF), pp. 7–17.
- VMCAI-2003-OgataF #protocol #verification
- Formal Verification of the Horn-Preneel Micropayment Protocol (KO, KF), pp. 238–252.
- FLOPS-2002-Futatsugi #formal method
- Formal Methods in CafeOBJ (KF), pp. 1–20.
- WRLA-2002-OgataF #authentication #protocol #verification
- Rewriting-Based Verification of Authentication Protocols (KO, KF), pp. 208–222.
- ASE-2001-OgataF #distributed #modelling #realtime #verification
- Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ (KO, KF), pp. 185–192.
- SAC-2000-OgataF #evaluation #on-demand #semantics
- Operational Semantics of Rewriting with the On-demand Evaluation Strategy (KO, KF), pp. 756–764.
- FM-v2-1999-DiaconescuFI #algebra #component #specification #verification
- Component-Based Algebraic Specification and Verification in CafeOBJ (RD, KF, SI), pp. 1644–1663.
- FM-v2-1999-MoriF #behaviour #specification #verification
- Verifying Behavioural Specifications in CafeOBJ Environment (AM, KF), pp. 1625–1643.
- SAC-1999-OgataIF #optimisation #term rewriting #using
- Optimizing Term Rewriting Using Discrimination Nets With Specialization (KO, SI, KF), pp. 511–518.
- FLOPS-1998-IshikawaWFMN #on the #semantics
- On the Semantics of GAEA (HI, TW, KF, JM, HN), pp. 123–142.
- WRLA-1998-DiaconescuF #overview
- An overview of CafeOBJ (RD, KF), pp. 285–298.
- WRLA-1998-MatsumotoF #automation #behaviour #induction #testing #towards #verification
- Test set coinduction — Toward automated verification of behavioural properties (MM, KF), pp. 242–262.
- ICSE-1997-NakajimaF #algebra #modelling #object-oriented #specification
- An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ (SN, KF), pp. 34–44.
- PLILP-1997-OgataF #evaluation #implementation #term rewriting
- Implementation of Term Rewritings with the Evaluation Strategy (KO, KF), pp. 225–239.
- RTA-1997-OgataOF #automaton #named #order #term rewriting
- TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems (KO, KO, KF), pp. 335–338.
- WRLA-J-1996-DiaconescuF02 #logic
- Logical foundations of CafeOBJ (RD, KF), pp. 289–318.
- ICSE-1990-NakagawaF #algebra #process
- Software Process à la Algebra: OBJ for OBJ (ATN, KF), pp. 12–23.
- ICSE-1989-NakagawaF #algebra #approach #composition #process #refinement
- Stepwise Refinement Process with Modularity: An Algebraic Approach (ATN, KF), pp. 166–177.
- ICSE-1988-NakagawaFTS #algebra #specification #using
- Algebraic Specification of Macintosh’s Quickdraw Using OBJ2 (ATN, KF, ST, TS), pp. 334–343.
- ICSE-1987-FutatsugiGMO #programming
- Parameterized Programming in OBJ2 (KF, JAG, JM, KO), pp. 51–60.
- POPL-1985-FutatsugiGJM
- Principles of OBJ2 (KF, JAG, JPJ, JM), pp. 52–66.
- ICSE-1982-FutatsugiO #functional
- A Hierarchical Structuring Method for Functional Software Systems (KF, KO), pp. 393–402.
- FASE-2016-RiescoOF #interpreter #maude #named
- CafeInMaude: A CafeOBJ Interpreter in Maude (AR0, KO0, KF), pp. 377–380.