Jump to contents

Researcher Information

last modified:2017/11/20

Professor YAMANE Satoshi

Mail Laboratory Website

Faculty, Affiliation

Faculty of Electrical and Computer Engineering, Institute of Science and Engineering

College and School Educational Field

Division of Electrical Engineering and Computer Science, Graduate School of Natural Science and Technology
Division of Electrical Engineering and Computer Science, Graduate School of Natural Science and Technology
School of Electrical and Computer Engineering, College of Science and Engineering

Laboratory

Computer software TEL:076-234-4856 FAX:076-234-4900

Academic Background

【Academic background(Doctoral/Master's Degree)】
Kyoto University Master 198403 Completed
【Academic background(Bachelor's Degree)】
Kyoto University
【Degree】
Dr. Eng.

Career

Kanazawa University faculty of engineering(2001/08/01-)

Year & Month of Birth

Academic Society



IEEE computer society
JIPS
IEICE
IEICE
IEICE
IEICE
IEICE
IEICE
IEICE
JIPS
IEICE
IEICE
IEICE
IEICE
IEICE
IEICE
IEICE
Language and Automaton
Information processing society of japan
japan society for software science and technology
The Institute of Electronic, Inforomation and Communication Engineers
The Institute of Electronic, Inforomation and Communication Engineers
IEICE
IEICE
The Japanese Society for Artificial Intelligence

Award

○GESTS best paper(2006/03/01)
○best paper of CST(2008/06/30)
○best paper of CST(2008/06/30)
○best paper of CST(2008/06/30)

Specialities

verification specification theory、Theory of informatics、Software、Computer system

Speciality Keywords

computer software, dynamic reconfigurable systems, model checking, real-time hybrid systems

Research Themes

design, verification and implementation of real-time software

design, verification and implementation of real-time software We study probabilistic timed CEGAR(CounterExample Guided Abstractuin and Refinement).

Formal modeling, specification and verification of embedded systems

Formal modeling, specification and verification of embedded systems We study modeling, specification and verification method for dynamically reconfigurable systems.
Also, we study dynamic hybrid CEGAR.

Distributed paralllel real-time systems

Books

  •  Hybrid automaton Ohmsha 7 1 21-29 2010/08

Papers

  •  A verification by strong probabilistic timed simulation relation using probabilistic zone graphs Y. Hashizume IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS 92 1 25-38 2009/01
  •  automatic verification of statecharts by abstraction and refinement of hierachical structure Shinichi Yamazaki 26 3 155-170 2009/08
  •  Case study of Modeling, Specification and Finite model checking for preemptive embedded software Shingo Takinai IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS 93 11 2403-2415 2010/11
  •  Case study of Modeling, Specification and Finite model checking for preemptive embedded software Masashi Hayashi I 93 7 1214-1225 2010/07
  •  Development Method for Real-Time Software based on Timed Weak Simulation Verification 2011/12

show all

  •  Specification and Verification Techniques of Embedded Systems using Probabilistic Linear Hybrid Automata Y. Mutsuda, T. Kato, S. Yamane 4 1 178-194 2006/01
  •  The automatic verification system for real-time systems using symbolic model-checking AMAST SERIES IN COMPUTING VOl.8 137-152 2007/03
  •  Theory and practice of probabilistic timed game for Embedded Systems LECTURE NOTES IN COMPUTER SCIENCE 4523,pp 109-120 2007/05
  •  Design analysis method of soft real-time systems using UML and timed automata Vol.48, No9,pp 2410-2421 2007/09
  •  Development of probabilistic timed strong simulation verifier of probabilistic timed automata Vol.25, No.3, pp 148-193 2008/08
  •  Modeling, Specification and Model checking of dynamically reconfigurable processors Computer Software 28 1 190-216 2011/01
  •  A method for the Specifications and Verification of Distributed Systems by Timed Automaton Systems and Computers in Japan 28 2 10 1997/12
  •  Automatic Verification Method for distributed and concurrent systems using timed language inclusion Journal of Parallel and Distributed Computing Practices 1 2 14 1998/06
  •  Study on verification method of statechart by fixpoint computation Systems and Computers in Japan 27 13 12 1997/06
  •  A Practical Hierachical Design by Timed Simulation Relations for Real-Time Systems LECTURE NOTES IN COMPUTER SCIENCE 1641 17 1999/10
  •  Hierarchical design method real-time distributed systems Proc. International Workshop on Real-Time Computing Systems and Applications 6 4 1998/11
  •  Modular Specification and Verification Method for Hybrid Real-time Systems Proc. International Conference on Real-Time Computing Systems and Applications 10 8 2002/03
  •  Specifications and Verification Method of Concurrent Systems by Restricted Timed Automaton S. Yamane LECTURE NOTES IN COMPUTER SCIENCE 1231 15 1997/05
  •  The symbolic model-checking for real-time systems Concurrency:theory and applications,RIMS,KYOTO University 996 21 1997/10
  •  Deductive Refinement Verification Methods based on Assume-Guarantee Style and their Experimental Evaluations of Real-Time Software International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computeing 2 8 2001/08
  •  Formal verification of real-time software by symbolic model checker International Conference on Application of Concurrency to System Design 1 10 1998/03
  •  Real-Time Symbolic Model Checking for Hard Real-Time Systems Proc. International Conference on Real-Time Computing Systems and Applications 7 4 1999/11
  •  Symbolic Model-checking method based on approximation and BDDs for real-time systems S. Yamane LECTURE NOTES IN COMPUTER SCIENCE 1281 23 1997/10
  •  Refinement Theory of Embedded systems based on Hybrid models 455-4 2002/06
  •  Formal development methodology of hybrid systems based on both control theory and computer science 469-4 2002/06
  •  Refinement Verification of Hybrid Automata for Embedded Systems 203-2 2003/01
  •  Formal Verification of schedulability of real-time software 209-2 2003/01
  •  Formal Probabilistic Refinement Verification Method of Embedded Real-Time Systems 1 1 79-82 2003/05
  •  Development and Evaluation of Symbolic Model-Checker Based on Approximation for Real-Time Systems 86 4 232-247 2003/04
  •  Formal refinement verification method of real-time systems with discrete probability distributions 2 202-215 2003/04
  •  Probabilistic Timed Simulation Verification and Its Application to Stepwise Refinement of Real-Time Systems LECTURE NOTES IN COMPUTER SCIENCE 2896 1 276-290 2003/12
  •  Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata IEE PROCEEDINGS-COMPUTERS AND DIGITAL TECHNIQUES 27 1 527-533 2003/11
  •  Formal Refinement verification method of real-time systems with discrete probability distributions 44 8 2189-2199 2003/08
  •  Probabilistic Timed Bisimulation relation and \\\\ 45 5 1201-127 2004/05
  •  Deductive Verification Method of Probabilistic Timed LTL 45 6 1421-1430 2004/06
  •  Deductive Probabilistic Verification Methods LECTURE NOTES IN COMPUTER SCIENCE 3207 1 163-195 2004/08
  •  Deductive Probabilistic Timed Verification 4 1 1-10 2005/04
  •  Refinement design method of real-time systems based on timed waek simulation verification. J88-D-I,No.10,pp 1555-1570 2005/10
  •  Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata Y. Mutsuda, T. Kato, S.Yamane Vol.E88-A No.11, pp 2972-2981 2005/11
  •  Performance analysis method of soft real-time systems by timed automata S. Yamane Vol.46, No11,pp 2410-2421 2005/11
  •  Timed Weak Simulation Verification and its application to Stepwise Refinement of Real-Time Software S. Yamane Vol.6, No.1B, pp 192-203 2006/01
  •  Automata-Theoretic Performance Analysis Method of Soft Real-Time Systems S. Yamane LECTURE NOTES IN COMPUTER SCIENCE 3823,pp 1211-1224 2005/11
  •  Timed Weak Simulation Verification and its application to Stepwise Refinement of Real-Time Software LECTURE NOTES IN COMPUTER SCIENCE 3824, pp 381-394 2005/11
  •  Deductive Probabilistic Verification Methods of Safety, Liveness and Nonzenoness for Distributed Real-Time Systems LECTURE NOTES IN COMPUTER SCIENCE 3820,pp 332-345 2005/12
  •  Formal verification of real-time systems 25 3 81-87 2008/08
  •  Specification and Verification Techniques of Embedded Systems using Probabilistic Linear Hybrid Automata Y. Mutsuda, T. Kato, S. Yamane LECTURE NOTES IN COMPUTER SCIENCE 3820,pp 346-360 2005/12
  •  Development of Model Checker of Dynamic Linear Hybrid Automata R.Yanase IEEE 37th COMPSAC 37 2013/07
  •  A New Approach to Specify and Verify Embedded Systems consisting of CPU and DRP R.Yanase The 18th IEEE Pacific Rim International Symposium on Dependable Computing 18 1-2 2012/08
  •  Trace-mining Profile for Large-Scale Distributed Framework Hadoop K.Sakurai The 18th IEEE Pacific Rim International Symposium on Dependable Computing 18 1-2 2012/08
  •  Development Method for Real-Time Software based on Timed Weak Simulation Verification Embedded Systems: Status and Perspective 1 1 2013/12
  •  Hybrid Automata Theoretic Specification and Verification of CPU-DRP Embedded Systems R.Yanase Bulletin of Networking, Computing, Systems, and Software 1 1 16-20 2012/12
  •  Rechability analysis of probabilistic linear hybrid automaton Journal of information processing society 53 12 2671-2681 2012/12
  •  Probabilistic Timed CEGAR Transaction on programming language 5 2 43-66 2012/03
  •  A method of generating traces of Hadoop YARN by lightweight profile data Yosuke Nakagawa, Kouhei Sakurai, Satoshi Yamane Annual Meeting on Advanced Computing System and Infrastructure 1-6 2015/01/26
  •  Fault-tolerant Performance Evaluation of Hadoop MapReduce by Fault-Injection Using AspectJ  Yosuke Nakagawa, Kohei Sakurai,Yusuke Shimizu, Satosahi Yamane Transaction on of IPSJ 7 1 35-45 2014/03/25  
  •  Specification language of dynamic reconfigurable systems Hidefumi Yamada, Yuki Nakai, Satoshi Yamane Transaction on programming language of IPSJ 6 3 1-19 2013/12/20 
  •  Development of Probabilistic Timed CEGAR Satoshi Yamane, Takaya Shimizu IEEE International Conference on Systems and Informatics 1-10 2014/11/19
  •  Model Generation by the Exhaustive Search for Embedded Assembly Programs and Application to Model Checking R.Konoshita, S. Yamane, K.Sakurai IEEE 3rd Global Conference on Consumer Electronics 1-4 2014/10/09
  •  Development of SMT-Based Bounded Model Checker for Embedded Assembly Program J.Kobashi, A.Takeshita, S.Yamane IEEE 3rd Global Conference on Consumer Electronics 1-4 2014/10/09
  •  Distributed Online Decision Tree Learning for Stream Data Based on Actor Model Koichi Yamamoto, Kohei Sakurai, Satoshi Yaman WebDB Forum 2014 1-8 2014/11/19
  •  SMT-Based Model Checking by Analyzing Embedded Assembly Program  J.Kobashi, A.Takeshita, S.Yamane EMBEDDED SYSTEM SYMPOSIUM2014 22-27 2014/10/23 
  •  Model Checking by Modeling for Embedded Assembly Programs  R.Konoshita, S. Yamane, K.Sakurai EMBEDDED SYSTEM SYMPOSIUM2014 13-21 2014/10/23 
  •  Invite paper: Deductively Verifying Embedded Software in the Era of Artificial Intelligence = Machine Learning + Software Science Satoshi Yamane IEEE GCCE2017 2017 1-4 2017/10/24
  •   Model checking of embedded assembly program based on simulation S.Yamane, R.Konoshita, T.Kato IEICE Transactions on Information and Systems  100 8 1819-1826 2017/08/01
  •  Recognition of Rotated Images by Angle Estimation Using Feature Map with CNN Nishiki Katayama, Satoshi Yamane IEEE GCCE2017 2017 1-4 2017/10/24
  •  Similarity Calculation for Face Verification with Convolutional Neural Network Nishiki Katayama, Satoshi Yamane SICE Annual Conference 2017 2017 2017/09/12
  •  Detecting Bank Conflict of GPU Programs Using Symbolic Execution - Case Study Khoki Hamaya, Satoshi Yamane Journal of Software Engineering and Applications 10 2 159-167 2017/02/21 
  •  A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata  Ryo Yanase, Tatsunori Sakai, Makoto Sakai and Satoshi Yamane Lecture Notes in Computer Science 10009 10009 74-89 2016/11/15 
  •  Abstraction Refinement for Non-Zeno Fairness Verification of Linear Hybrid Automata R.Yanase, S.Yamane 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)Doctoral Symposium 10 1 2017/03/17 
  •  Speci cation and veri cation of Dynamically Recon gurable Systems using Dynamic Linear Hybrid Automata Ryo Yanase, Tatsunori Sakai, Makoto Sakai, Satoshi Yamane Journal of Software Engineering and Applications 2016 9 452-478 2016/09/30 
  •  Simulation and Model checking of embedded assembly program Satoshi Yamane,Tomonori Kato,Ryosuke Konoshita ESS2016 2016/10/20
  •  Integration of Supervised and Unsupervised Learning for Deep Neural Network T.Uchiyama, S.Yamane,K.Sakurai,T.Kurita The Korea-Japan joint workshop on Frontiers of Computer Vision (FCV) 2016/02/23
  •  LogChamber: Inferring Source Code Locations Corresponding to Mobile Applications Run-time Logs Yuki Ono, Kouhei Sakurai, Satoshi Yamane:  Journal of Information Processing 24 4 700-710 2016/07/07
  •   Detecting Bank Conflict of GPU Programs Using Symbolic Execution K.Hamaya, S.Yamane IEEE 5th Global Conference on Consumer Electronics (GCCE 2015) 5 1-3 2016/10/12 
  •  Formal Verification of Dynamically Reconfigurable Systems  R.Yanase, T.Sakai,M.Sakai,S.Yaname IEEE 4th Global Conference on Consumer Electronics (GCCE 2015) 4 2015/10 
  •   Distributed CFG-based Symbolic Execution for Assembly Programs  T.Adachi, S.Yamane, K.Sakurai IEEE 4th Global Conference on Consumer Electronics (GCCE 2015) 4 76-80 2015/10 
  •  Parallel Distributed Graph Clustering Algorithm on Apache Spark with Node Partition and Aggregation in Large-Scale Graphs R.Asayama, K.Sakurai,S.Yamane International Workshop on Innovative Algorithms for Big Data 1 1 1-2 2015/09

Conference Presentations

  • Deductive Verification methods of real-time properties for embedded assembly program(2017/06/20)
  • Verification method of real-time properties for embedded assembly program(conference:IEICE Technical Reprt MSS2016)(2017/03/16)

Arts and Fieldwork

Patent

Theme to the desired joint research

Grant-in-Aid for Scientific Research

○「時相論理と並行計算,オートマトンの統合化による自律性のある分散システムの設計支援」(1999-2001) 
○「ハイブリッドモデルによる組込みシステムの高信頼性設計方法論の構築と支援環境の開発」(2002-2004) 
○「述語抽象化検証による大規模組込みシステム向きオブジェクト指向設計自動検証手法」(2007-2009) 
○「音響心理の定量的計測を目標とした心理モデルの構築と実験的検討」(1997-1998) 
○「動的ハイブリッドオートマトンによる動的再構成可能組込みシステムの高度な設計検証」(2012-2014) 

Classes (Bachelors)

○Computer System(2017)
○Operating Systems(2017)
○Distributed Computing(2017)
○Compiler(2017)
○Computer System(2017)
○Distributed Computing(2016)
○Compiler(2016)
○Operating Systems(2016)
○Computer System(2016)
○study in undergraduate course(2016)
○study in undergraduate course(2015)
○Operating System(2015)
○Compiler(2015)
○Disributed Computing(2015)
○Computer System(2015)
○study in undergraduate course(2014)
○Computer system(2014)
○Compiler(2014)
○Operating system(2014)
○Principle of software science(2014)
○study in undergraduate course(2013)
○study in undergraduate course(2013)
○Special lecture of infromation system(2013)
○Operating system(2013)
○Computer system(2013)
○Introduction(2013)
○Introduction to electronic, information system and bioinfomatics(2013)
○Compiler(2013)
○Principle of software science(2013)

Classes (Graduate Schools)

○Verification of Distributed, Parallel and Real-Time Systems(2017)
○Verification of Distributed, Parallel and Real-Time Systems(2017)
○Verification of Distributed, Parallel and Real-Time Systems(2017)
○Verification of Distributed, Parallel and Real-Time Systems(2017)
○Distributed parallel real-time systems(2017)
○Distributed parallel real-time systems(2016)
○Verification of Distributed, Parallel and Real-Time Systems(2016)
○Design and verification of distributed real-time systems(2015)
○Distributed, parallel and real-time system(2015)
○Design and verification of distributed and real-time system(2014)
○Verification theory(2014)
○Special lecture on sofutoware science(2014)
○Verification theory(2013)
○Distributed and real-time systems(2013)
○Software Engineering(2013)

International Project

International Students

Lecture themes

Others (Social Activities)

To Page Top