Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
123 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ. |
ASE |
2001 |
DBLP DOI BibTeX RDF |
modeling, verification, specification, algebraic specification, distributed real-time systems, UNITY, CafeOBJ |
116 | Kokichi Futatsugi |
Formal Methods in CafeOBJ. |
FLOPS |
2002 |
DBLP DOI BibTeX RDF |
|
116 | Razvan Diaconescu, Kokichi Futatsugi, Shusaku Iida |
Component-Based Algebraic Specification and Verification in CafeOBJ. |
World Congress on Formal Methods |
1999 |
DBLP DOI BibTeX RDF |
|
80 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm. |
APAQS |
2001 |
DBLP DOI BibTeX RDF |
modeling, verification, distributed algorithms, specification, algebraic specification, UNITY, CafeOBJ |
79 | Jianwen Xiang, Dines Bjørner, Kokichi Futatsugi |
Formal digital license language with OTS/CafeOBJ method. |
AICCSA |
2008 |
DBLP DOI BibTeX RDF |
|
79 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method. |
Essays Dedicated to Joseph A. Goguen |
2006 |
DBLP DOI BibTeX RDF |
|
79 | Kokichi Futatsugi |
Verifying Specifications with Proof Scores in CafeOBJ. |
ASE |
2006 |
DBLP DOI BibTeX RDF |
|
69 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Proof Scores in the OTS/CafeOBJ Method. |
FMOODS |
2003 |
DBLP DOI BibTeX RDF |
observational transition system, proof scores, the NSLPK authentication protocol, verification, Algebraic specification, CafeOBJ |
62 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes. |
ICFEM |
2008 |
DBLP DOI BibTeX RDF |
observational transition system (OTS), verification, mutual exclusion, invariant property, CafeOBJ |
62 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Formal Analysis of the NetBill Electronic Commerce Protocol. |
ISSS |
2003 |
DBLP DOI BibTeX RDF |
NetBill, OTS, verification, electronic commerce, security protocol, algebraic specification, CafeOBJ |
61 | Kazuhiro Ogata 0001, Masahiro Nakano, Masaki Nakamura 0001, Kokichi Futatsugi |
Chocolat/SMV: A Translator from CafeOBJ into SMV. |
PDCAT |
2005 |
DBLP DOI BibTeX RDF |
|
55 | Weiqiang Kong, Kazuhiro Ogata 0001, Jianwen Xiang, Kokichi Futatsugi |
Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol. |
CIT |
2004 |
DBLP DOI BibTeX RDF |
|
55 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Formal Verification of the Horn-Preneel Micropayment Protocol. |
VMCAI |
2003 |
DBLP DOI BibTeX RDF |
|
55 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Formal Verification of the MCS List-Based Queuing Lock. |
ASIAN |
1999 |
DBLP DOI BibTeX RDF |
|
50 | Shin Nakajima 0001, Kokichi Futatsugi |
An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ. |
ICSE |
1997 |
DBLP DOI BibTeX RDF |
concurrent rewriting, excutable specifications, object-oriented modelinng, formal methods, algebraic specifications, OBJ, CafeOBJ |
44 | Iakovos Ouranos, Petros S. Stefaneas |
Verifying Security Protocols for Sensor Networks Using Algebraic Specification Techniques. |
CAI |
2007 |
DBLP DOI BibTeX RDF |
Algebraic Specification and Verification, Observational Transition Systems, SPINS Protocol suite, Sensor Networks, CafeOBJ |
44 | Kazuhiro Ogata 0001, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi |
Induction-Guided Falsification. |
ICFEM |
2006 |
DBLP DOI BibTeX RDF |
observational transition system (OTS), invariant, induction, counterexample, Maude, CafeOBJ |
43 | Tetsuo Tamai |
Formal Treatment of a Family of Fixed-Point Problems on Graphs by CafeOBJ. |
ICFEM |
2000 |
DBLP DOI BibTeX RDF |
|
43 | Akira Mori, Kokichi Futatsugi |
Verifying Behavioural Specifications in CafeOBJ Environment. |
World Congress on Formal Methods |
1999 |
DBLP DOI BibTeX RDF |
|
36 | Weiqiang Kong, Kazuhiro Ogata 0001, Kokichi Futatsugi |
Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System. |
IFM |
2007 |
DBLP DOI BibTeX RDF |
|
36 | Shin Nakajima 0001 |
Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks. |
World Congress on Formal Methods |
1999 |
DBLP DOI BibTeX RDF |
|
26 | Xiaoyi Chen, Weiqiang Kong, Kokichi Futatsugi |
Formal support for e-government system design with transparency consideration. |
ICEGOV |
2007 |
DBLP DOI BibTeX RDF |
license language, the OTS/CafeOBJ method, formal methods, domain engineering, public administration |
25 | Yifan Wang, Masaki Nakamura 0001, Kazutoshi Sakakibara, Yuki Okura |
Formal Specification and Verification of an Autonomous Vehicle Control System by the OTS/CafeOBJ method (S). |
SEKE |
2023 |
DBLP DOI BibTeX RDF |
|
25 | Masaki Nakamura 0001, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata 0001 |
Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method. |
IEICE Trans. Fundam. Electron. Commun. Comput. Sci. |
2022 |
DBLP DOI BibTeX RDF |
|
25 | Adrián Riesco 0001, Kazuhiro Ogata 0001 |
An integrated tool set for verifying CafeOBJ specifications. |
J. Syst. Softw. |
2022 |
DBLP DOI BibTeX RDF |
|
25 | Kokichi Futatsugi |
Advances of proof scores in CafeOBJ. |
Sci. Comput. Program. |
2022 |
DBLP DOI BibTeX RDF |
|
25 | Tatsuya Igarashi, Masaki Nakamura 0001, Kazutoshi Sakakibara |
Formal Verification of the Lim-Jeong-Park-Lee Autonomous Vehicle Control Protocol using the OTS/CafeOBJ Method. |
SEKE |
2022 |
DBLP DOI BibTeX RDF |
|
25 | Duong Dinh Tran, Dang Duy Bui, Kazuhiro Ogata 0001 |
Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method. |
IEEE Access |
2021 |
DBLP DOI BibTeX RDF |
|
25 | Kokichi Futatsugi |
Advances of Proof Scores in CafeOBJ. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
25 | Masaki Nakamura 0001, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata 0001 |
Formal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method. |
Int. J. Softw. Eng. Knowl. Eng. |
2021 |
DBLP DOI BibTeX RDF |
|
25 | Masaki Nakamura 0001, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata 0001 |
Formal verification of multitask hybrid systems by the OTS/CafeOBJ method. |
SEKE |
2021 |
DBLP DOI BibTeX RDF |
|
25 | Kokichi Futatsugi |
Advances of Proof Scores in CafeOBJ : Invited Paper. |
TASE |
2021 |
DBLP DOI BibTeX RDF |
|
25 | Masaki Nakamura 0001, Kazutoshi Sakakibara, Kazuhiro Ogata 0001 |
Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
25 | Duong Dinh Tran, Kazuhiro Ogata 0001 |
Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG. |
SEKE |
2020 |
DBLP DOI BibTeX RDF |
|
25 | Adrián Riesco 0001, Kazuhiro Ogata 0001 |
CiMPG+F: A Proof Generator and Fixer-Upper for CafeOBJ Specifications. |
ICTAC |
2020 |
DBLP DOI BibTeX RDF |
|
25 | Masaki Nakamura 0001, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata 0001 |
Formal verification of Fischer's real-time mutual exclusion protocol by the OTS/CafeOBJ method. |
SICE |
2020 |
DBLP BibTeX RDF |
|
25 | Nikolaos Triantafyllou |
Software engineering applications of the OTS/CafeOBJ algebraic specification method |
|
2019 |
RDF |
|
25 | Adrián Riesco 0001, Kazuhiro Ogata 0001 |
Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. |
ACM Trans. Softw. Eng. Methodol. |
2018 |
DBLP DOI BibTeX RDF |
|
25 | Dominik Klein 0001 |
Key-Secrecy of PACE with OTS/CafeOBJ. |
IACR Cryptol. ePrint Arch. |
2018 |
DBLP BibTeX RDF |
|
25 | Adrián Riesco 0001, Kazuhiro Ogata 0001, Kokichi Futatsugi |
A Maude environment for CafeOBJ. |
Formal Aspects Comput. |
2017 |
DBLP DOI BibTeX RDF |
|
25 | Xuan-Linh Ha, Kazuhiro Ogata 0001 |
Writing Concurrent Java Programs Based on CafeOBJ Specifications. |
APSEC |
2017 |
DBLP DOI BibTeX RDF |
|
25 | Ryusei Mori, Masaki Nakamura 0001 |
Automated Test Case Generation from OTS/CafeOBJ Specifications by Specification Translation. |
ICST Workshops |
2017 |
DBLP DOI BibTeX RDF |
|
25 | Masaki Nakamura 0001 |
A preliminary study of test case generation by CafeOBJ rewrite specifications. |
GCCE |
2016 |
DBLP DOI BibTeX RDF |
|
25 | Adrián Riesco 0001, Kazuhiro Ogata 0001, Kokichi Futatsugi |
CafeInMaude: A CafeOBJ Interpreter in Maude. |
FASE |
2016 |
DBLP DOI BibTeX RDF |
|
25 | Kokichi Futatsugi |
Generic Proof Scores for Generate & Check Method in CafeOBJ. |
Logic, Rewriting, and Concurrency |
2015 |
DBLP DOI BibTeX RDF |
|
25 | Kokichi Futatsugi |
Generate & Check Method for Verifying Transition Systems in CafeOBJ. |
Software, Services, and Systems |
2015 |
DBLP DOI BibTeX RDF |
|
25 | Iakovos Ouranos, Kazuhiro Ogata 0001, Petros S. Stefaneas |
TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned. |
IEICE Trans. Inf. Syst. |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Dominik Klein 0001 |
Key-Secrecy of PACE with OTS/CafeOBJ. |
FTSCS |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Yongxin Zhao, Jin Song Dong, Yang Liu 0003, Jun Sun 0001 |
Towards a Combination of CafeOBJ and PAT. |
Specification, Algebra, and Software |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Daniel Gâinâ, Dorel Lucanu, Kazuhiro Ogata 0001, Kokichi Futatsugi |
On Automation of OTS/CafeOBJ Method. |
Specification, Algebra, and Software |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Petros S. Stefaneas, Iakovos Ouranos, Nikolaos Triantafyllou, Katerina Ksystra |
Some Engineering Applications of the OTS/CafeOBJ Method. |
Specification, Algebra, and Software |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Razvan Diaconescu |
CafeOBJ Traces. |
Specification, Algebra, and Software |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Till Mossakowski, Wieslaw Pawlowski, Donald Sannella, Andrzej Tarlecki |
Parchments for CafeOBJ Logics. |
Specification, Algebra, and Software |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Min Zhang 0002, Kazuhiro Ogata 0001, Kokichi Futatsugi |
Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method. |
Specification, Algebra, and Software |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Adrián Riesco 0001 |
An Integration of CafeOBJ into Full Maude. |
WRLA |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Norbert Preining, Kazuhiro Ogata 0001, Kokichi Futatsugi |
Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications. |
LOPSTR |
2014 |
DBLP DOI BibTeX RDF |
|
25 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method. |
J. Univers. Comput. Sci. |
2013 |
DBLP DOI BibTeX RDF |
|
25 | Kokichi Futatsugi, Daniel Gâinâ, Kazuhiro Ogata 0001 |
Principles of proof scores in CafeOBJ. |
Theor. Comput. Sci. |
2012 |
DBLP DOI BibTeX RDF |
|
25 | Iakovos Ouranos, Kazuhiro Ogata 0001, Petros S. Stefaneas |
Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method. |
ISoLA (2) |
2012 |
DBLP DOI BibTeX RDF |
|
25 | Konstantinos Barlas, George Koletsos, Petros S. Stefaneas |
Transforming ASN.1 Specifications into CafeOBJ to assist with Property Checking |
CoRR |
2011 |
DBLP BibTeX RDF |
|
25 | Weiqiang Kong, Kazuhiro Ogata 0001, Kokichi Futatsugi |
Towards Reliable E-Government Systems with the OTS/CafeOBJ Method. |
IEICE Trans. Inf. Syst. |
2010 |
DBLP DOI BibTeX RDF |
|
25 | Konstantinos Barlas, George Koletsos, Petros S. Stefaneas, Iakovos Ouranos |
Towards a correct translation from ASN.1 into CafeOBJ. |
Int. J. Reason. based Intell. Syst. |
2010 |
DBLP DOI BibTeX RDF |
|
25 | Kokichi Futatsugi |
Fostering Proof Scores in CafeOBJ. |
ICFEM |
2010 |
DBLP DOI BibTeX RDF |
|
25 | Iakovos Ouranos, Petros S. Stefaneas, Kazuhiro Ogata 0001 |
Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method. |
ISoLA (1) |
2010 |
DBLP DOI BibTeX RDF |
|
25 | Nikolaos Triantafyllou, Iakovos Ouranos, Petros S. Stefaneas, Panayiotis Frangos |
Formal Specification and Verification of the OMA License Choice Algorithm in the OTS/CafeOBJ Method. |
WINSYS |
2010 |
DBLP BibTeX RDF |
|
25 | Nikolaos Triantafyllou, Iakovos Ouranos, Petros S. Stefaneas, Panayiotis Frangos |
Using the OTS/CafeOBJ Method to Formally Specify and Verify the Open Mobile Alliance License Choice Algorithm. |
ICETE (Selected Papers) |
2010 |
DBLP DOI BibTeX RDF |
|
25 | Masaki Nakamura 0001, Takahiro Seino |
Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method. |
IEICE Trans. Inf. Syst. |
2009 |
DBLP DOI BibTeX RDF |
|
25 | Weiqiang Kong, Kazuhiro Ogata 0001, Jian Cheng, Kokichi Futatsugi |
Trace anonymity in the OTS/CafeOBJ method. |
CIT |
2008 |
DBLP DOI BibTeX RDF |
|
25 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method. |
REFINE@IFM |
2007 |
DBLP DOI BibTeX RDF |
|
25 | Samira Sadaoui, Sudhanshu Singh |
Implementation of CafeOBJ Specifications to Java Code. |
SEKE |
2006 |
DBLP BibTeX RDF |
|
25 | Antonio Carvalho Júnior, Leila Silva, Márcio Cornélio |
Using CafeOBJ to Mechanise Refactoring Proofs and Application. |
SBMF |
2005 |
DBLP DOI BibTeX RDF |
|
25 | Takahiro Seino, Kazuhiro Ogata 0001, Kokichi Futatsugi |
A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method. |
RULE@RDP |
2005 |
DBLP DOI BibTeX RDF |
|
25 | Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata 0001, Kokichi Futatsugi |
Provably Correct Translation from CafeOBJ into Java. |
SEKE |
2005 |
DBLP BibTeX RDF |
|
25 | André Luis Silva, Manoel Messias Menezes, Leila Silva |
Using CafeOBJ to Implement a Reduction Strategy in the Context of Hardware/Software Partitioning. |
WMF |
2003 |
DBLP DOI BibTeX RDF |
|
25 | Razvan Diaconescu, Kokichi Futatsugi, Kazuhiro Ogata 0001 |
CafeOBJ: Logical Foundations and Methodologies. |
Comput. Artif. Intell. |
2003 |
DBLP BibTeX RDF |
|
25 | Chartchai Doungsa-ard, Taratip Suwannasart |
An Automatic Approach to Transform CafeOBJ Specifications to Java Template Code. |
Software Engineering Research and Practice |
2003 |
DBLP BibTeX RDF |
|
25 | Toshimi Sawada, Kouichi Kishida, Kokichi Futatsugi |
Past, Present, and Future of SRA Implementation of CafeOBJ: Annex. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
25 | Razvan Diaconescu, Kokichi Futatsugi |
Logical foundations of CafeOBJ. |
Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
25 | Akira Mori, Kokichi Futatsugi |
CafeOBJ as a Tool for Behavioral System Verification. |
ISSS |
2002 |
DBLP DOI BibTeX RDF |
|
25 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Specifying and verifying a railroad crossing with CafeOBJ. |
IPDPS |
2001 |
DBLP DOI BibTeX RDF |
|
25 | Razvan Diaconescu, Kokichi Futatsugi |
An overview of CafeOBJ. |
WRLA |
1998 |
DBLP DOI BibTeX RDF |
|
25 | Razvan Diaconescu, Kokichi Futatsugi |
Cafeobj Report - The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification |
|
1998 |
DOI RDF |
|
18 | Francisco Durán 0001, Salvador Lucas, Claude Marché, José Meseguer 0001, Xavier Urbain |
Proving operational termination of membership equational programs. |
High. Order Symb. Comput. |
2008 |
DBLP DOI BibTeX RDF |
Conditional term rewriting, Operational termination, Declarative rule-based languages, Program transformation, Membership equational logic |
18 | Deirdre Carew, Chris Exton, Jim Buckley |
An empirical investigation of the comprehensibility of requirements specifications. |
ISESE |
2005 |
DBLP DOI BibTeX RDF |
|
18 | Kazuhiro Ogata 0001, Kokichi Futatsugi |
Equational Approach to Formal Analysis of TLS. |
ICDCS |
2005 |
DBLP DOI BibTeX RDF |
security, verification, algebraic specification, rewriting, interactive theorem proving |
18 | Francisco Durán 0001, Salvador Lucas, José Meseguer 0001, Claude Marché, Xavier Urbain |
Proving termination of membership equational programs. |
PEPM |
2004 |
DBLP DOI BibTeX RDF |
program transformation, termination, term rewriting, membership equational logic |
18 | Jianwen Xiang, Kokichi Futatsugi, Yanxiang He |
Fault Tree and Formal Methods in System Safety Analysis. |
CIT |
2004 |
DBLP DOI BibTeX RDF |
|
18 | Razvan Diaconescu |
Behavioural Specification for Hierarchical Object Composition. |
FMCO |
2003 |
DBLP DOI BibTeX RDF |
|
18 | María Alpuente, Santiago Escobar 0001, Bernhard Gramlich, Salvador Lucas |
Improving On-Demand Strategy Annotations. |
LPAR |
2002 |
DBLP DOI BibTeX RDF |
on-demand strategy annotations, lazy evaluation, Declarative programming, demandness, OBJ |
18 | Grigore Rosu |
On implementing behavioral rewriting. |
ACM SIGPLAN Workshop on Rule-Based Programming |
2002 |
DBLP DOI BibTeX RDF |
behavioral rewriting, hidden equational logic, term rewriting, meta-programming |
18 | Bernhard Gramlich, Salvador Lucas |
Simple termination of context-sensitive rewriting. |
ACM SIGPLAN Workshop on Rule-Based Programming |
2002 |
DBLP DOI BibTeX RDF |
automatic proofs of termination, context-sensitive rewriting, modular program analysis and verification, declarative programming, evaluation strategies |
18 | Bernhard Gramlich, Salvador Lucas |
Modular termination of context-sensitive rewriting. |
PPDP |
2002 |
DBLP DOI BibTeX RDF |
context-sensitive rewriting, modular analysis and construction of programs, modular proofs of termination, program verification, declarative programming, evaluation strategies |