Search results for "CafeOBJ"

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