Kazuhiro Ogata
Orcid: 0000-0002-4441-3259Affiliations:
- Japan Advanced Institute of Science and Technology (JAIST), Nomi, Japan
- Keio University, Yokohama, Japan (PhD 1995)
According to our database1,
Kazuhiro Ogata
authored at least 171 papers
between 1992 and 2024.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis Dataset OtherLinks
Online presence:
-
on orcid.org
On csauthors.net:
Bibliography
2024
Integration of state machine graphical animation and Maude to facilitate characteristic conjecture: an approach to lemma discovery in theorem proving.
Multim. Tools Appl., April, 2024
IEEE Access, 2024
2023
ACM Trans. Softw. Eng. Methodol., November, 2023
Selected papers from the 15th international symposium on Theoretical Aspects of Software Engineering (TASE 2021).
Sci. Comput. Program., 2023
Transport Layer Security 1.0 handshake protocol formal verification case study: How to use a proof script generator for existing large proof scores.
PeerJ Comput. Sci., 2023
Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version.
PeerJ Comput. Sci., 2023
PeerJ Comput. Sci., 2023
J. Vis. Lang. Comput., 2023
Proceedings of the 35th International Conference on Software Engineering and Knowledge Engineering, 2023
A way to find counterexamples located at deep positions with domain knowledge of authentication protocols.
Proceedings of the 12th International Conference on Software and Computer Applications, 2023
Proceedings of the 12th International Conference on Software and Computer Applications, 2023
Proceedings of the 29th International DMS Conference on Visualization and Visual Languages, 2023
Proceedings of the Dynamic Logic. New Trends and Applications - 5th International Workshop, 2023
2022
Multim. Tools Appl., 2022
Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol.
J. Vis. Lang. Comput., 2022
Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method.
IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2022
Comput. Secur., 2022
Comput. J., 2022
Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way.
IEEE Access, 2022
Proceedings of the Rewriting Logic and Its Applications - 14th International Workshop, 2022
Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude.
Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering, 2022
Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering, 2022
Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis.
Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols co-located with the 23rd International Conference on Formal Engineering Methods (ICFEM 2022), 2022
Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude.
Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols co-located with the 23rd International Conference on Formal Engineering Methods (ICFEM 2022), 2022
Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude.
Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols co-located with the 23rd International Conference on Formal Engineering Methods (ICFEM 2022), 2022
Proceedings of the 9th International Conference on Dependable Systems and Their Applications, 2022
Proceedings of the 28th International DMS Conference on Visualization and Visual Languages, 2022
Proceedings of the 28th International DMS Conference on Visualization and Visual Languages, 2022
Proceedings of the 46th IEEE Annual Computers, Software, and Applications Conferenc, 2022
2021
J. Vis. Lang. Comput., 2021
Int. J. Softw. Eng. Knowl. Eng., 2021
IEEE Access, 2021
Proceedings of the 33rd International Conference on Software Engineering and Knowledge Engineering, 2021
Proceedings of the 33rd International Conference on Software Engineering and Knowledge Engineering, 2021
Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S).
Proceedings of the 33rd International Conference on Software Engineering and Knowledge Engineering, 2021
Proceedings of the 21st IEEE International Conference on Software Quality, 2021
Proceedings of the Theoretical Aspects of Computing - ICTAC 2021, 2021
Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S).
Proceedings of the 27th International DMS Conference on Visualization and Visual Languages, 2021
Proceedings of the 27th International DMS Conference on Visualization and Visual Languages, 2021
A support tool for the L + 1-layer divide & conquer approach to leads-to model checking.
Proceedings of the IEEE 45th Annual Computers, Software, and Applications Conference, 2021
2020
Stability of termination and sufficient-completeness under pushouts via amalgamation.
Theor. Comput. Sci., 2020
Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions.
J. Inf. Secur. Appl., 2020
A Generic Approach on How to Formally Specify and Model Check Path Finding Algorithms: Dijkstra, A* and LPA.
Int. J. Softw. Eng. Knowl. Eng., 2020
Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method.
CoRR, 2020
Formal verification of Fischer's real-time mutual exclusion protocol by the OTS/CafeOBJ method.
Proceedings of the 59th Annual Conference of the Society of Instrument and Control Engineers of Japan, 2020
Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG.
Proceedings of the 32nd International Conference on Software Engineering and Knowledge Engineering, 2020
Proceedings of the 20th IEEE International Conference on Software Quality, 2020
Proceedings of the Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30, 2020
Proceedings of the 27th Asia-Pacific Software Engineering Conference, 2020
Proceedings of the 27th Asia-Pacific Software Engineering Conference, 2020
2019
J. Vis. Lang. Comput., 2019
A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions.
Frontiers Comput. Sci., 2019
A More Faithful Formal Definition of the Desired Property for Distributed Snapshot Algorithms to Model Check the Property.
Comput. Informatics, 2019
Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2019
Proceedings of the Structured Object-Oriented Formal Language and Method, 2019
Proceedings of the Structured Object-Oriented Formal Language and Method, 2019
Proceedings of the 31st International Conference on Software Engineering and Knowledge Engineering, 2019
Proceedings of the 31st International Conference on Software Engineering and Knowledge Engineering, 2019
Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S).
Proceedings of the 31st International Conference on Software Engineering and Knowledge Engineering, 2019
Proceedings of the Fundamental Approaches to Software Engineering, 2019
2018
ACM Trans. Softw. Eng. Methodol., 2018
From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories.
Theor. Comput. Sci., 2018
Formal analysis of a security protocol for e-passports based on rewrite theory specifications.
J. Inf. Secur. Appl., 2018
Proceedings of the 7th International Conference on Software and Computer Applications, 2018
Guessing Properties of the Qlock Mutual Exclusion Protocol based on its Graphical Animations and confirming the Properties by Model Checking.
Proceedings of the 7th International Conference on Software and Computer Applications, 2018
Model Checking of the Suzuki-Kasami Distributed Mutual Exclusion Algorithm with SPIN.
Proceedings of the 5th International Conference on Dependable Systems and Their Applications, 2018
Analysis of Some Variants of the Anderson Array-Based Queuing Mutual Exclusion Protocol with Model Checking and Graphical Animations.
Proceedings of the 5th International Conference on Dependable Systems and Their Applications, 2018
Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks.
Proceedings of the 25th Asia-Pacific Software Engineering Conference, 2018
2017
Proceedings of the Structured Object-Oriented Formal Language and Method, 2017
A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2017
Proceedings of the 2017 International Conference on Software Analysis, 2017
Proceedings of the 21st International Conference on Principles of Distributed Systems, 2017
Proceedings of the Theoretical Aspects of Computing - ICTAC 2017, 2017
Specifying a Distributed Snapshot Algorithm as a Meta-Program and Model Checking it at Meta-Level.
Proceedings of the 37th IEEE International Conference on Distributed Computing Systems, 2017
Proceedings of the 15th IEEE Intl Conf on Dependable, 2017
Proceedings of the 24th Asia-Pacific Software Engineering Conference, 2017
2016
Formal modeling and analysis of time- and resource-sensitive simple business processes.
J. Inf. Secur. Appl., 2016
Proceedings of the Structured Object-Oriented Formal Language and Method, 2016
Proceedings of the Fundamental Approaches to Software Engineering, 2016
2015
Case Studies on Extracting the Characteristics of the Reachable States of State Machines Formalizing Communication Protocols with Inductive Logic Programing.
Proceedings of the Late Breaking Papers of the 25th International Conference on Inductive Logic Programming, 2015
Proceedings of the Formal Methods and Software Engineering, 2015
Proceedings of the Advances in Computer Science and Ubiquitous Computing, 2015
Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates.
Proceedings of the 2015 Asia-Pacific Software Engineering Conference, 2015
2014
TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned.
IEICE Trans. Inf. Syst., 2014
A Formal Semantics of the OSEK/VDX Standard in $${\mathbb {K}}$$ Framework and Its Applications.
Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014
Proceedings of the Logic-Based Program Synthesis and Transformation, 2014
Proceedings of the Specification, Algebra, and Software, 2014
Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications.
Proceedings of the Specification, Algebra, and Software, 2014
Proceedings of the Specification, Algebra, and Software, 2014
Proceedings of the Specification, Algebra, and Software, 2014
Proceedings of the 21st Asia-Pacific Software Engineering Conference, 2014
2013
J. Univers. Comput. Sci., 2013
Formalization and Verification of Behavioral Correctness of Dynamic Software Updates.
Proceedings of the 2013 Validation Strategies for Software Evolution Workshop, 2013
Proceedings of the 37th Annual IEEE Computer Software and Applications Conference, 2013
Proceedings of the 20th Asia-Pacific Software Engineering Conference, 2013
2012
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, 2012
Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic.
Proceedings of the Formal Methods and Software Engineering, 2012
Proceedings of the 19th Asia-Pacific Software Engineering Conference, 2012
Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules.
Proceedings of the 19th Asia-Pacific Software Engineering Conference, 2012
2011
Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support.
IEICE Trans. Inf. Syst., 2011
2010
Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications.
J. Symb. Comput., 2010
Int. J. Softw. Eng. Knowl. Eng., 2010
IEICE Trans. Inf. Syst., 2010
Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010
Specification Translation of State Machines from Equational Theories into Rewrite Theories.
Proceedings of the Formal Methods and Software Engineering, 2010
Proceedings of the Formal Methods and Software Engineering, 2010
2009
Modular Implementation of a Translator from Behavioral Specifications to Rewrite Theory Specifications.
Proceedings of the Ninth International Conference on Quality Software, 2009
Proceedings of the Algebra and Coalgebra in Computer Science, 2009
2008
IEICE Trans. Inf. Syst., 2008
A Specification Translation from Behavioral Specifications to Rewrite Specifications.
IEICE Trans. Inf. Syst., 2008
Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes.
Proceedings of the Formal Methods and Software Engineering, 2008
Proceedings of 8th IEEE International Conference on Computer and Information Technology, 2008
2007
Sci. Comput. Program., 2007
Int. J. Softw. Eng. Knowl. Eng., 2007
Int. J. Softw. Eng. Knowl. Eng., 2007
IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2007
Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm.
IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2007
Proceedings of the BCS-FACS Refinement Workshop, 2007
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007
2006
Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management.
Proceedings of the WEBIST 2006, 2006
Falsification of OTSs by Searches of Bounded Reachable State Spaces.
Proceedings of the Eighteenth International Conference on Software Engineering & Knowledge Engineering (SEKE'2006), 2006
Proceedings of the Sixth International Conference on Quality Software (QSIC 2006), 2006
Proceedings of the Formal Methods and Software Engineering, 2006
Proceedings of the Algebra, Meaning, and Computation, 2006
2005
Int. J. Pervasive Comput. Commun., 2005
Proceedings of the 6th International Workshop on Rule-Based Programming, 2005
Proceedings of the Verified Software: Theories, 2005
Provably Correct Translation from CafeOBJ into Java.
Proceedings of the 17th International Conference on Software Engineering and Knowledge Engineering (SEKE'2005), 2005
Formal Analysis of Workflow Systems with Security Considerations.
Proceedings of the 17th International Conference on Software Engineering and Knowledge Engineering (SEKE'2005), 2005
Proceedings of the Fifth International Conference on Quality Software (QSIC 2005), 2005
Proceedings of the Sixth International Conference on Parallel and Distributed Computing, 2005
Proceedings of the 25th International Conference on Distributed Computing Systems (ICDCS 2005), 2005
Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 2005
A Lightweight Integration of Theorem Proving and Model Checking for System Verification.
Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 2005
Proceedings of the Fifth International Conference on Computer and Information Technology (CIT 2005), 2005
2004
Proceedings of the 4th International Conference on Quality Software (QSIC 2004), 2004
Proceedings of the Design Methods and Applications for Distributed Embedded Systems, 2004
Proceedings of the 2004 International Conference on Computer and Information Technology (CIT 2004), 2004
Proceedings of the 2004 International Conference on Computer and Information Technology (CIT 2004), 2004
2003
Inf. Process. Lett., 2003
Proceedings of the Verification, 2003
Proceedings of the Software Security, 2003
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2003
2002
Proceedings of the Fourth International Workshop on Rewriting logic and Its Applications, 2002
Proceedings of the Software Security -- Theories and Systems, 2002
Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems V, 2002
2001
Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001
Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01), 2001
Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm.
Proceedings of the 2nd Asia-Pacific Conference on Quality Software (APAQS 2001), 2001
2000
Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, 2000
Proceedings of the Applied Computing 2000, 2000
1999
Proceedings of the 1999 ACM Symposium on Applied Computing, 1999
Proceedings of the Advances in Computing Science, 1999
1998
Proceedings of the Euro-Par '98 Parallel Processing, 1998
1997
Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997
Proceedings of the Programming Languages: Implementations, 1997
Proceedings of the Euro-Par '97 Parallel Processing, 1997
1994
Proceedings of the 1994 ACM Symposium on Applied Computing, 1994
1992
HoME: Smalltalk on the Match Environment.
Proceedings of the TOOLS 1992: 6th International Conference on Technology of Object-Oriented Languages and Systems, 1992
Proceedings of the ACM SIGPLAN'92 Conference on Programming Language Design and Implementation (PLDI), 1992