TOP Page >  Profile

To Lab's Site


Full text / JAIST Repository



Toshiaki Aoki Professor
School of Transdisciplinary Sciences、School of Information Science、Security and Networks Area


B.S. from Science University of Tokyo(1994), M.S. and Ph.D. from Japan Advanced Institute of Science and Technology(1996, 1999)


Software Engineering, Software Science, Formal Method, Formal Verification

■Research Interests

Principle of Software
Fundamental theories for software are studying for a long time. Some of them are getting matured such as program semantics and process algebra. To promise bright future of software, it is important to find the principles of software based on those theories. Unfortunately, today’s software is developed without such principles. We should change this style of software developments into more scientific ones which are integrated on the mathematics. Thus, we are challenging to establish such fundamental principles of software.
Formal Method/Formal Verification
Formal methods represent a development style of software based onmathematics. We describe its specification and design in not naturallanguage but languages based on mathematical theories such as sets andfunctions. That not only makes the specification and design rigorous butalso allows us to precisely analyze them, prove their correctness andautomatically generate source codes. One way to provide correctness withsoftware is that we describe it rigorously, then we prove itscorrectness. That is called 'formal verification' of software. We areresearching how we can develop correct software effectively using theformal methods and formal verification. Especially, we focus on embeddedsystems and object-oriented design for their application targets.



  • Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods,Toshiaki Aoki, Kenji Taguchi (Eds.),Lecture Notes in Computer Science 7635, Springer,2012

◇Published Papers

  • SMT-based enumeration of Object Graphs from UML Class Diagrams,Kenro Yatake, Toshiaki Aoki,UML&FM,August 27, 2012
  • Model Checking of OSEK/VDX OS Design Models based on Environment Modeling,Kenro Yatake, Toshiaki Aoki,ICTAC,Sep 25, 2012
  • Automatic Generation of Model Checking Scripts based onEnvironment Modeling,Kenro Yatake, Toshiak Aoki,SPIN 2010, LNCS,Vol. 6349,pp. 58-75

Display All

■Extramural Activities

◇Other Activities

  • IEICE,SIGSS Steering Committee,2008/04/01 - 2010/03/31
  • IPSJ SIGEMB,Steering Committee,2007/04/01 - 2010/03/31
  • JSSST,Computer Software Journal Editorial Board,2007/04/01 -

Display All