Yoshinao Isobe
Senior Researcher
Software Analytics Research Team
Cyber Physical Security Research Center
National Institute of Advanced Industrial Science and Technology (AIST)
Software Analytics Research Team
Cyber Physical Security Research Center
National Institute of Advanced Industrial Science and Technology (AIST)
Kansai Center, 1831 Midorigaoka, Ikeda, Osaka 5638577 Japan
Email: yisobe@aist.go.jp
[Japanese Page]Email: yisobe@aist.go.jp

CSPProver:
A generic theorem prover of CSP refinemnet
(in cooperation with Prof. Markus Roggenbach) 
RWSolver
:A tool for generating train timetables with the help of SMTSolver
(in cooperation with JREast)  CoopRobo : Formal modeling and verification of cooperative transport robots
 Machine Learning Quality Evaluation and Improvement (Technical Report)
 Y. Isobe, N. Miyamoto, N. Ando, and Y. Oiwa, Formal Modeling and Verification of Concurrent FSMs: Case Study on EventBased Cooperative Transport Robots, IEICE Transactions on Information and Systems, Vol.E104D, No.10, pp.15151532, 2021. [PDF (4.6MB)]
 Y. Isobe, H. Hatsugai, A. Tanaka, Y. Oiwa, T. Ambe, A. Okada, S. Kitamura, Y. Fukuta, and T. Kunifuji, Automatic Generation of Train Timetables from Mesoscopic Railway Models by SMTSolver, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol.E102A, No.2, pp.325335, 2019. [PDF (5.5MB)]
 T. Kaizu, Y. Isobe, M. Suzuki, SDVerifier: A tool for verification of sequence diagrams using the process algebra CSP (Japanese), JSSST (Japan Society for Software Science and Technology) Computer Software, Vol.32, No.1, pp.234252, 2015.
 A. Sampaio, S. Nogueira, A. Mota, Y. Isobe, Sound and Mechanised Compositional Verification of InputOutput Conformance, Journal of Software Testing, Verification and Reliability, 24(4), pp.289319, 2014.

T. Kaizu, Y. Isobe, M. Suzuki,
Refinement and Verification of Sequence Diagrams Using the Process Algebra CSP,
IEICE Transactions on Fundamentals, Vol. E96A(2): 496504, 2012.

Y. Isobe, F. Moller, H. N. Nguyen, M. Roggenbach,
Safety and Line Capacity in Railways  An Approach in Timed CSP,
In 9th International Conference on Integrated Formal Methods (IFM 2012), LNCS 7321, pp.5468, Springer, 2012

Y. Isobe,
CONPASUtool:
A Concurrent Process Analysis Support Tool based on Symbolic Computation,
In 33th WoTUG Conference on Communicating Process Architectures (CPA 2011), pp. 341362, 2011
 L.
O'Reilly, Y. Isobe, M. Roggenbach,
CSPCASLProver  A Generic Tool for Process and Data Refinement,
Electronic Notes in Theoretical Computer Science, 250(2), pp.6984, 2009.
 G. Samuel, Y. Isobe, M. Roggenbach, The Stable Revival Model in CSPProver, Electronic Notes in Theoretical Computer Science, 250(2), pp.119134, 2009.
 Y. Isobe and M.Roggenbach, CSPProver  a Proof Tool for the Verification of Scalable Concurrent Systems, Journal of Computer Software, Japan Society for Software Science and Technology (JSSST), Vol.25, No.4, pp.8592, 2008.
 Y. Isobe and M. Roggenbach, Proof Principles of CSP  CSPProver in Practice, Dynamics in Logistics: First International Conference, LDIC 2007, Springer, pp.425422, 2007.

Y. Isobe and M. Roggenbach,
A complete axiomatic semantics for the CSP stablefailures model,
CONCUR 2006
(17th International Conference on Concurrency Theory),
LNCS 4137, Springer, pp.158172, Bonn (Germany), August 2006.

Y. Isobe and M. Roggenbach,
A Generic Theorem Prover of CSP Refinement,
TACAS 2005
(
11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems),
LNCS 3440,
pp.108123, Edinburgh, April 2005. [PDF: 254KB]
 Y. Isobe and K. Ohmaki, A Noninterleaving Timed Process Algebra and a Process Logic for Verifying Composition of Agents (full version), JSSST (Japan Society for Software Science and Technology) Computer Software, Vol.20, No.5, pp.5879, 2003. [PDF: 355KB]
 Y. Isobe and K. Ohmaki, A Noninterleaving Timed Process Algebra and a Process Logic for Verifying Composition of Agents, IFICT2003 (1st International Forum on Information and Computer Technology), pp.215220, 2003. [PDF: 140KB]
 Y. Isobe and K. Ohmaki, A Process Logic for Distributed System Synthesis, APSEC 2000 (7th AsiaPacific Software Engineering Conference), IEEE Computer Society Press. pp.6269, 2000. [PDF: 138KB]
 Y. Isobe, Y. Sato, and K. Ohmaki, Least Fixpoint and Greatest Fixpoint in a Process Algebra with Conjunction and Disjunction, IEICE (Institute of Electronics, Information and Communication Engineers) Trans. on Fundamentals, Vol.E83A, No.3, pp.401411, 2000. [PDF: 205KB]
 Y. Isobe, Y. Sato, and K. Ohmaki, Eventuality in LOTOS with a Disjunction Operator, ASIAN'98 (4th Asian Computing Science Conference), LNCS 1538, SpringerVerlag, pp.263281, 1998. [PDF: 195KB]
 Y. Isobe, Y. Sato, and K. Ohmaki, Approximative Analysis by Process Algebra with Graded Spatial Actions (Japanese), JSSST (Japan Society for Software Science and Technology) Computer Software, Vol.14, No.2, pp.421, 1997. [PDF: 269KB]
 Y. Isobe, Y. Sato, and K. Ohmaki, Approximative Analysis by Process Algebra with Graded Spatial Actions, AMAST'96 (Fifth International Conference on Algebraic Methodology and Software Technology), LNCS 1101, SpringerVerlag, pp.336350, 1996. [PDF: 220KB]
 Y. Isobe, Y. Sato, and K. Ohmaki, A Calculus of Countable Broadcasting Systems (Japanese), JSSST (Japan Society for Software Science and Technology) Computer Software, Vol.13, No.1, pp.5570, 1996. [PDF: 214KB]
 Y. Isobe, Y. Sato, and K. Ohmaki, A Calculus of Countable Broadcasting Systems, AMAST'95 (Fourth International Conference on Algebraic Methodology and Software Technology), LNCS 936, SpringerVerlag, pp.489503, 1995. [PDF: 165KB]
 Y. Isobe, I. Kojima, and K. Ohmaki, Analysis of Database Production Rules by Process Algebra, IEICE (Institute of Electronics, Information and Communication Engineers) Trans. Information and Systems. Vol.E78D, No.8, pp.9921002, 1995. [PDF: 203KB]