PUBLICATION 研究業績

論文誌

  • Charnon Pattiyanon and Toshiaki Aoki: Compliance SSI System Property Set to Laws, Regulations, and Technical Standards, in IEEE Access, vol. 10, pp. 99370-99393, 2022, doi: 10.1109/ACCESS.2022.3204112.

  • Jingcheng Yuan, Toshiaki Aoki, Xiaoyun Guo: Comprehensive evaluation of file systems robustness with SPIN model checking, Journal of Software: Testing, Verification and Reliability, 32(6) , 2022.

  • Thuy Nguyen, Takashi Tomita, Junpei Endo, Toshiaki Aoki: Integrating Pattern Matching and Abstract Interpretation for Verifying Cautions of Microcontrollers, Journal of Software: Testing, Verification and Reliability, 31(8), Wiley, Aug. 19, 2021.

  • Zhengguo Yang, Toshiaki Aoki, Yasuo Tan: Multiple conformance to hybrid-automata-modelled requirements for detecting indoor temperature anomalies, Indoor and Built Environment, 25 pages, August 9, 2020.

  • Hoang Viet Tran, Pham Ngoc Hung, Viet Ha Nguyen, and Toshiaki Aoki: A framework for assume-guarantee regression verification of evolving software, Science of Computer Programming, Vo. 193, July, 2020.

  • Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi and Toshiaki Aoki: Template-Based Monte-Carlo Test-Suite Generation for Large and Complex Simulink Models, IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences, Vol.E103-A No.2, pp.451-461, Feb., 2020.

  • Xiaoyun Guo, Toshiaki Aoki and Hsin-Hung Lin: Model checking of in-vehicle networking systems with CAN and FlexRay, Journal of Systems and Software, Volume 161, Feb., 2020,

  • Tran Nhat-Hoa, Yuki Chiba and Toshiaki Aoki: Model Checking in the Presence of Schedulers Using a Domain Specific Language for Scheduling Policies, IEICE Transactions, Vol.E102-D,No.7, pp.1280-1295, Jul., 2019.

  • Pattaravut Maleehuan, Yuki Chiba, Toshiaki Aoki: A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT Solver. IEICE Transactions 101-D(12): 3038-3058 (2018).

  • 青木利晃:車載システム開発における形式手法実践の現状と課題,システム/制御/ 情報,第62巻,第4号,pp. 134-140,システム制御情報学会,2018.

  • Haitao Zhang, Toshiaki Aoki, Yuki Chiba: Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach, IEICE Transactions, Volume 98-D, No.10, pp.1765-1776, October, 2015.

  • Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki:A Framework for Verifying the Conformance of Design to Its Formal Specifications, IEICE Transactions, Volume E98-D No.6, pp.1137-1149, June, 2015.

  • Warawoot Pacharoen, Toshiaki Aoki, Pattarasinee Bhattarakosol, and Athasit Surarerks, Active Learning of Nondeterministic Finite State Machines, Mathematical Problems in Engineering, vol. 2013, Article ID 373265, 11 pages, 2013. doi:10.1155/2013/373265

  • Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama: On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification, IEICE Transactions, Vol.95-A, No.9, pp.1451-1460, 2012.

  • 矢竹健朗, 青木利晃: UMLに基づくRTOS設計検証のための環境自動生成法, 日本ソフトウェア科学会 学会誌 コンピュータソフトウェア,Vo.29, No.3, p.121-142, 2012.

  • Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama: Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking, IEICE Transactions Vol.E95-D,No.7, pp.1882-1893, Jul., 2012.

  • Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama: A Minimized Assumption Generation Method for Component-Based Software Verification, IEICE Transactions Vol.E93-D,No.8,pp.2172-2181, Aug. 2010.

  • Pham Ngoc Hung, Toshiaki Aoki, Takuya Katayama: Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based Software, IEICE Transactions Vol.E92-A, No.11, pp.2772-2780, Nov., 2009.

  • Hideaki Nishihara, Koichi Shinozaki, Koji Hayamizu, Toshiaki Aoki, Kenji Taguchi, Fumihiro Kumeno:Model checking education for software engineers in Japan, ACM SIGCSE Bulletin, Volume 41 , Issue 2 (June 2009), p.45-50, 2009.

  • Yasuyuki Tahara, Nobukazu Yoshioka, Kenji Taguchi, Toshiaki Aoki, Shinichi Honiden: Evolution of a course on model checking for practical applications, ACM SIGCSE Bulletin, Volume 41 , Issue 2 (June 2009), p.38-44, 2009.

  • 青木利晃: 高信頼性組み込みソフトウェア開発-最新技術動向と取り組み:2.形式的 手法による高信頼性組み込みソフトウェア開発, 情報処理学会 学会誌 Vol.47 No.5, p. 491-497, 2006.

  • Takuya Katayama, Tatsuo Nakajima, Taichi Yuasa, Tomoji Kishi, Shin Nakajima, Shuichi Oikawa, Masahiro Yasugi, Toshiaki Aoki, Mitsutaka Okazaki and Seiji Umatani: Highly Reliable Embedded Software Development Using Advanced Software Technologies, IEICE Transactions on Information and Systems, Vol.E88-D, No.6, p.1105-1116, June, 2005.

  • 岡崎光隆,青木利晃,片山卓也:並行オブジェクトから並行処理列への変換法,日 本ソフトウェア科学会 学会誌 コンピュータソフトウェア,Vo.22, No.2, p.58-73, 2005.

  • 矢竹健朗,青木利晃,片山卓也:コラボレーションに基づくオブジェクト指向モデ ルの検証,日本ソフトウェア科学会 学会誌 コンピュータソフトウェア,Vol.22, No.1,p.58-76, 2005.

  • 青木利晃,片山卓也:オブジェクト指向分析モデルにおけるデータフローの形式化 と解析手法 ,日本ソフトウェア科学会 学会誌 コンピュータソフトウェア, Vol.21,No.4,p.1-26, July, 2004.

  • 立石孝彰, 青木利晃, 片山卓也:振舞い近似手法を用いたステートチャートに対す る不変性の検証,情報処理学会論文誌 Vol.44 No.6,p.1448-1460,2003.

  • 青木利晃, 立石 孝彰, 片山卓也:定理証明技術のオブジェクト指向分析への適用, 日本ソフトウェア科学会学会誌 コンピュータソフトウェア, Vol.18 No.4,p.18-47, 2001.

  • 青木利晃, 内藤壮司, 片山卓也: オブジェクト指向組み込みシステム開発のためのSes-Basedアプローチ,日本ソフト ウェア科学会学会誌 コンピュータソフトウェア, Vol.16 No.2,p.67-71, 1999

  • 青木利晃, 片山卓也: オブジェクト指向方法論のための形式的モデル, 日本ソフトウェア科学会学会誌 コンピュータソフトウェア Vol.16, No.1,p.12-32, 1999.

国際会議

  • Yuki Yamaguchi, Toshiaki Aoki: Attack Tree Analysis for Adversarial Evasion Attacks, IEEE Pacific Rim International Symposium on Dependable Computing (PRDC), pp.46-52, 2023.

  • Kazunori Someya, Toshiaki Aoki, Naoki Ishihama: Compaction of Spacecraft Operational Models with Metamodeling Domain Knowledge, International Conference on Evaluation of Novel Approaches to Software Engineering, pp.102-113, 2023.

  • Kento Tanaka, Toshiaki Aoki, Tatsuji Kawai, Takashi Tomita, Daisuke Kawakami and Nobuo Chida: Specification Based Testing of Object Detection for Automated Driving Systems via BBSL, International Conference Evaluation of Novel Approaches to Software Engineering, pp.250-261, 2023.

  • Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do and Hideaki Takai: Coverage Testing of Industrial Simulink Models Using Monte-Carlo and SMT-Based Methods, International Conference on Software Quality, Reliability, and Security (QRS), pp.422-433, 2022.

  • Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai: SMT-Based Model Checking of Industrial Simulink Models, International Conference on Formal Engineering Method (ICFEM), pp.156-172, 2022.

  • Thuy Nguyen, Takashi Tomita, Junpei Endo, Geon-ung Kang, Toshiaki Aoki: Leveraging hardware-dependent knowledge extraction with multiple program analysis techniques, Symposium On Applied Computing (SAC), pp. 1827-1836, 2022.

  • Daisuke Ishii, Takashi Tomita, Toshiaki Aoki: Approximate Translation from Floating-Point to Real-Interval Arithmetic. NASA Formal Methods(NFM), pp. 733-751, 2022.

  • Kento Tanaka, Toshiaki Aoki, Tatsuji Kawai, Takashi Tomita, Daisuke Kawakami, Nobuo Chida: A Formal Specification Language Based on Positional Relationship Between Objects in Automated Driving Systems, COMPSAC, pp.950-955, 2022.

  • Charnon Pattiyanon, Toshiaki Aoki, Daisuke Ishii: A Method for Detecting Common Weaknesses in Self-Sovereign Identity Systems Using Domain-Specific Models and Knowledge Graph, 10th International Conference on Model-Driven Engineering and Software Development(MODELSWARD), pp.219-226, 2022.

  • Charnon Pattiyanon, Toshiaki Aoki: Analysis and Enhancement of Self-sovereign Identity System Properties Compiling Standards and Regulations, 8th International Conference on Information Systems Security and Privacy (ICISSP), pp. 133-144, 2022.

  • Nhat-Hoa Tran, Toshiaki Aoki: SSpinJa: Facilitating Schedulers in Model Checking, 21th IEEE International Conference on Software Quality, Reliability, and Security(QRS), pp. 632-641, 2021.

  • Toshiaki Aoki, Daisuke Kawakami, Nobuo Chida, Takashi Tomita: Dataset Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems, 25th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC), pp.100-109, 2020.

  • Kenji Fujita, Kunihiko Hiraishi, Toshiaki Aoki: Frequency Probabilistic Risk Assessment Using Coloured Petri Nets for Telemedicine, IEEE International Conference on Industrial Engineering and Engineering Management(IEEM), 2020, to appear.

  • Jingcheng Yuan, Toshiaki Aoki and Xiaoyun Guo: Comprehensive Robustness Evaluation of File Systems with Model Checking, IEEE 20th International Conference on Software Quality, Reliability, and Security (QRS), pp.99-110, 2020.

  • Thuy Nguyen, Toshiaki Aoki, Takashi Tomita and Junpei Endo: Integrating Static Program Analysis Tools for Verifying Cautions of Microcontroller, Asia-Pacific Software Engineering Conference(APSEC), pp.86-93, 2019.

  • Thu-Trang Nguyen, Toshiaki Aoki, Takashi Tomita and Iori Yamada: Multiple Program Analysis Techniques Enable Precise Check for SEI CERT C Coding Standard, Asia-Pacific Software Engineering Conference(APSEC), pp.70-77, 2019.

  • Nhat-Hoa Tran and Toshiaki Aoki: Conformance Testing of Schedulers for DSL-based Model Checking, 26th International SPIN Symposium on Model Checking of Software, pp. 208-225, 2019.

  • Kazunori Someya, Naoki Ishihama, Keiichi Wada, Toshiaki Aoki: Compaction of Spacecraft Operation Model using Domain Knowledge based Stereotype, International Symposium on Space Technology and Science, 2019.

  • Thu Trang Nguyen, Pattaravut Maleehuan, Toshiaki Aoki, Takashi Tomita, Iori Yamada: Reducing False Positives of Static Analysis for SEI CERT C Coding Standard, Joint International Workshop on Conducting Empirical Studies in Industry (CESI) and 6th International Workshop on Software Engineering Research and Industrial Practice (SER&IP), pp. 41-48, 2019.

  • Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki: A Scalable Monte-Carlo Test-Case Generation Tool for Large and Complex Simulink Models, 11th Workshop on Modelling in Software Engineering (MiSE), pp.39-46, 2019.

  • Zhengguo Yang, Toshiaki Aoki, Yasuo Tan, Modeling the Required Indoor Temperature Change by Hybrid Automata for Detecting Thermal Problems, The 23rd IEEE Pacific Rim International Symposium on Dependable Computing(PRDC), pp. 135-145, 2018.

  • Zhengguo Yang, Toshiaki Aoki, Yasuo Tan: Multiple Conformance to Hybrid Automata for Checking Smart House Temperature Change, IEEE/ACM the 22nd International Symposium on Distributed Simulation and Real Time Applications(DS-RT), pp.1-10, 2018.

  • Trinh Le Khanh, Yuki Chiba and Toshiaki Aoki: Formalization and Verification of AUTOSAR OS Standard's Memory Protection, The 12th International Symposium on Theoretical Aspects of Software Engineering, pp. 68-75, 2018.

  • Nhat-Hoa Tran, Yuki Chiba and Toshiaki Aoki: Qualitative and Quantitative Analysis with Scheduling Policies in Model Checking, The 33rd ACM/SIGAPP Symposium On Applied Computing(SAC), Software Verification and Testing Track, pp.1873-1880, 2018.

  • Xiaoyun Guo, Hsin-Hung Lin, Toshiaki Aoki and Yuki Chiba: A Reusable Framework for Modeling and Verifying In-vehicle Networking System in the Presence of CAN and FlexRay, 24th Asia-Pacific Software Engineering Conference(APSEC), 2017(to appear).

  • Nhat-Hoa Tran, Yuki Chiba and Toshiaki Aoki: Domain-Specific Language Facilitates Scheduling in Model Checking, 24th Asia-Pacific Software Engineering Conference(APSEC), 2017(best paper award)(to appear)

  • Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi and Toshiaki Aoki: Template-Based Monte-Carlo Test Generation for Simulink Models, Seventh Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy'17), 2017(to appear).

  • Pattaravut Maleehuan, Yuki Chiba and Toshiaki Aoki: Assembly Program Verification for Multiprocessors with Relaxed Memory Model using SMT Solver, 11th International Symposium on Theoretical Aspects of Software Engineering(TASE 2017), 2017(to appear).

  • Dieu Huong Vu, Yuki Chiba, Kenro Yatake and Toshiaki Aoki: Verifying OSEK/VDX OS Design using Its Formal Specification, International Symposium on Theoretical Aspects of Software Engineering, pp.81-88, 2016.

  • Toshiaki Aoki, Kriangkrai Traichaiyaporn, Yuki Chiba, Masahiro Matsubara, Masataka Nishi and Fumio Narisawa: Modeling Safety Requirements of ISO26262 using Goal Trees and Patterns, International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS), Springer CCIS, pp.206-221, 2015.

  • Hideto Ogawa, Makoto Ichii, Fumihiro Kumeno, Toshiaki Aoki: Experimental Fault Analysis Process Implemented Using Model Extraction and Model Checking, COMPSAC, pp.95-104, 2015.

  • Haitao Zhang, Toshiaki Aoki, Yuki Chiba: Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications, IEEE International Conference on Software Testing, Verification and Validation(ICST), pp.1-10, 2015.

  • Haitao Zhang, Toshiaki Aoki, and Yuki Chiba: A Spin-based Approach for Checking OSEK/VDX Applications, Third International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS), 2014.

  • Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, and Toshiaki Aoki: Checking the Conformance of a Promela Design to Its Formal Specification in Event-B, Third International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS), 2014.

  • Hideto Ogawa, Makoto Ichii, Fumihiko Kumeno and Toshiaki Aoki: A Practical Study of Debugging using Model Checking, Industry Track, 20th Asia-Pacific Software Engineering Conference(APSEC), pp.134-139, 2013.

  • Kriangkrai Traichaiyaporn and Toshiaki Aoki: Preserving correctness of requirements evolution through refinement in Event-B, 20th Asia-Pacific Software Engineering Conference(APSEC), pp.315-322, 2013.

  • Haitao Zhang, Toshiaki Aoki, Hsin-Hung Lin, Min Zhang, Yuki Chiba and Kenro Yatake: SMT-based Bounded Model Checking for OSEK/VDX Applications, 20th Asia-Pacific Software Engineering Conference(APSEC), pp.307-314, 2013.

  • Xiaoyun Guo, Hsin-Hung Lin, Kenro Yatake and Toshiaki Aoki An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol, Second International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS), Communications in Computer and Information Science(CCIS), Volume 419, Springer, pp.36-53, 2014(presented in 2013).

  • Kriangkrai Traichaiyaporn and Toshiaki Aoki: Refinement Tree and Its Patterns: a Graphical Approach for Event-B Modeling, Second International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS), Communications in Computer and Information Science(CCIS), Volume 419, Springer, pp.246-261, 2014 (presented in 2013).

  • Hirokazu Yatsu, Takahiro Ando, Weiqiang Kong, Kenji Hisazumi, Akira Fukuda, Toshiaki Aoki, Kokichi Futatsugi: Towards Formal Description of Standards for Automotive Operating Systems, ICST Workshops, pp.13-14, 2013.

  • Kenji Taguchi, Hideaki Nishihara, Toshiaki Aoki, Fumihiro Kumeno, Koji Hayamizu, Koichi Sinozaki:Building A Body of Knowledge on Model Checking for Software Development, Proceedings of Annual International Computers, Software & Applications Conference (COMPSAC), pp.784-789, 2013.

  • Haitao Zhang, Toshiaki Aoki, Kenro Yatake, Min Zhang and Hsin-Hung Lin: An approach for checking OSEK/VDX applications, The 13th International Conference on Quality Software(QSIC), pp.113-116, 2013.

  • Shinji Kikuchi and Toshiaki Aoki: Evaluation of Operational Vulnerability in Cloud Service Management using Model Checking, IEEE Seventh International Symposium on Service-Oriented System Engineering(SOSE), pp.37-48, 2013.

  • Kenro Yatake, Toshiaki Aoki: Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling, International Colloquium on Theoretical Aspect of Computing(ICTAC), pp.183-197, 2012.

  • Kenro Yatake, Toshiaki Aoki: SMT-based Enumeration of Object Graphs from UML class diagrams, 5th International workshop UML and Formal Methods, ACM SIGSOFT Software Engineering Notes, Vol.37, Issue 4, pp.1-8, 2012.

  • Dieu-Huong Vu, Toshiaki Aoki: Faithfully Formalizing OSEK/VDX Operating System Specification, third International Symposium on Information and Communication Technology(SoICT 2012), pp.13-20, 2012.

  • Hiroaki Tanizaki, Toshiaki Aoki and Takuya Katayama: A Variability Management Method for Software Configuration Files, The 24th International Conference on Software Engineering and Knowledge Engineering(SEKE 2012), pp.672-677, 2012.

  • Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama: An Improvement of Minimized Assumption Generation Method for Component-Based Software Verification. The 9th IEEE-RIVF International Conference on Computing and Communication Technologies(RIVF 2012),pp.1-6, 2012.

  • Jiang Chen and Toshiaki Aoki: Conformance Testing for OSEK/VDX Operating System Using Model Checking, 18th Asia-Pacific Software Engineering Conference(APSEC 2011), pp.274-281, 2011.

  • Warawoot Pacharoen, Toshiaki Aoki, Athasit Surarerks and Pattarasinee Bhattarakosol: Conformance Verification between Web Service Choreography and Implementation Using Learning and Model Checking, IEEE International Conference on Web Services(ICWS 2011), pp.722-723, 2011.

  • Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama: Automated Adaptor Generation for Services Based on Pushdown Model Checking, 18th IEEE International Conference and Workshops on Engineering of Computer-Based Systems(ECBS 2011), pp.130-139, 2011.

  • Pham Ngoc Hung, Nguyen Viet Ha, Toshiaki Aoki and Takuya Katayama: Assume-Guarantee Tools for Component-Based Software Verification, The second International Conference on Knowledge and Systems Engineering(KSE 2010), pp. 172-177, 2010.

  • Kenro Yatake and Toshiaki Aoki: Automatic Generation of Model Checking Scripts based on Environment Modeling, The 17th International SPIN Workshop on Model Checking of Software (SPIN 2010), pp.58-75, 2010.

  • Chaiwat Sathawornwichit, Toshiaki Aoki and Takuya Katayama: Modeling of Real-Time System Designs for Parametric Analysis, the 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications(RTCSA 2010), pp.81-91, 2010.

  • Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama: Non-Regular Adaptation of Services Using Model Checking, IEEE International Symposium on Object-Oriented/Component/Service-oriented Real-Time Distributed Computing(ISORC 2010), pp.170-174, 2010.

  • Pham Ngoc Hung, Toshiaki Aoki and Takuya Katayama: An effective framework for assume-guarantee verification of evolving component-based software, Proceedings of the joint international and annual ERCIM workshops on Principles of software evolution (IWPSE) and software evolution (Evol) workshops, p.109-118, 2009.

  • Pham Ngoc Hung, Toshiaki Aoki and Takuya Katayama: A Minimized Assumption Generation Method for Component-Based Software Verification, In the 6th International Colloquium on Theoretical Aspect of Computing, LNCS 5684, pp.277-291, Springer-Verlag, 2009.

  • Toshiaki Aoki, Tadashi Sekiguchi, Masayuki Hirayama, and Tomoji Kishi: Detecting and Analyzing State Inconsistencies in Multi-task Software, 12th IEEE International Symposium on Object-Oriented/Component/Service-oriented Real-Time Distributed Computing, pp.326-330, 2009.

  • Yasuyuki Tahara, Nobukazu Yoshioka, Kenji Taguchi, Toshiaki Aoki, and Shinichi Honiden: Education Course of Practical Model Checking, First International Workshop on Formal Methods Education and Training, 2008, pp.33-48, 2008.

  • Hideaki Nishihara, Koichi Shinozaki, Koji Hayamizu, Toshiaki Aoki, Kenji Taguchi, Fumihiro Kumeno:Model checking education for software engineers in Japan, First International Workshop on Formal Methods Education and Training, 2008, pp.49-58, 2008.

  • Toshiaki Aoki: Model Checking Multi-task Software on Real-time Operating Systems, International Symposium on Object-Oriented Real-Time Distributed Computing 2008, p.551-555, 2008.

  • Toshiaki Aoki and Takuya Katayama: Statechart-based Verification of Object-Oriented Design Models, 14th Asia-Pacific Software Engineering Conference, p.278--285, 2007.

  • Kenro Yatake, Toshiaki Aoki and Takuya Katayama: Implementing aplication-specific Object-Oriented theories in HOL, International Colloquium on Theoretical Aspects of Computing, p.501-516, 2005.

  • Toshiaki Aoki and Takuya Katayama: Formalization and Analysis of Dataflow in Object-Oriented Design Models, International Symposium on Object-Oriented Real-Time Distributed Computing 2005, p.95-105, 2005.

  • Toshiaki Aoki and Takuya Katayama: Foundations for Evolutionary Construction of State Transition Models, the Seventh International Workshop on Principles of Software Evolution 2004, p.143-146, 2004.

  • Tomoji Kishi, Toshiaki Aoki, Shin Nakajima, Natsuko Noda and Takuya Katayama: Project Report: High-Reliable Object-Oriented Embedded Software Design, The 2nd IEEE Workshop on Software Technologies for Embedded and Ubiquitous Computing Systems, 2004.

  • Kenro Yatake, Toshiaki Aoki and Takuya Katayama: Collaboration-based Verfication of Object-Oriented models in HOL, Proceedings of the 2nd International Workshop on Verification and Validation of Enterprise Information Systems, VVEIS 2004, p.78-80, 2004.

  • Mitsutaka Okazaki, Toshiaki Aoki and Takuya Katayama : Formalizing sequence diagrams and state machines using Concurrent Regular Expression: Proceedings of 2nd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools SCESM’03, p.74-79, 2003

  • Mitsutaka Okazaki, Toshiaki Aoki and Takuya Katayama: Extracting threads from concurrent objects for the design of embedded systems, Ninth Asia-Pacific Software Engineering Conference 2002, p.107-116, 2002.

  • Takaaki Tateishi, Toshiaki Aoki and Takuya Katayama: Successive Behavior Aproximation Method for Verifying Distributed Objects, Third International Conference on Parallel and Distributed Computing, Aplications and Technologies, p.439-446, 2002.

  • Toshiaki Aoki, Takaaki Tateishi and Takuya Katayama: An Axiomatic Formalization of UML Models, Practical UML-Based Rigorous Development Methods, p.13-28, 2001.

  • Toshiaki Aoki and Takuya Katayama: Prototype Execution of Independently Constructed Object-Oriented Analysis Model ,ECOOP2001 Workshop Automating the Object-Oriented Software Development Methods, p.25-33, 2001.

  • Takaaki Tateishi, Toshiaki Aoki and Takuya Katayama: An Axiomatic System For Verifying The Object-Oriented Analysis Model, SCI2000, p.662-667, 2000.

  • Toshiaki Aoki and Takuya Katayama: SES Model for Object-Oriented Time Critical System Development, International Conference on Artificial and Computational Intelligence for Decision, Control and Automation in Engineering and Industrial Aplications(ACIDCA2000), p.19-24, 2000.

  • Toshiaki Aoki, Masaki Hamada and Takuya Katayama: How to suport verification of object-oriented analysis models using HOL, Sci/ISAS'99, p.525-532, 1999.

  • Toshiaki Aoki, Akira Kawaguchi, Tomoji Kishi and Takuya Katayama: Synchronized Execution Sequence Based Software Architecture for Object-Oriented Embedded Systems, Position Paper for WICSA1, 1999.

  • Toshiaki Aoki and Takuya Katayama: Unification and Consistency Verification of Object-Oriented Analysis Models, APSEC'98, p.296-303, 1998.

  • Toshiaki Aoki and Takuya Katayama: Formal Model Aproach for Reliable Object-Oriented Information System Design, Sci/ISAS'98, p.228-235, 1998.

書籍

  • Toshiaki Aoki, Makoto Satoh, Mitsuhiro Tani, Kenro Yatake, Tomoji Kishi: Combined Model Checking and Testing Create Confidence-A Case on Commercial Automotive Operating System, pp.109-132, Cyber-Physical System Design from an Architecture Analysis Viewpoint, Springer, 2017.

  • Toshiaki Aoki, Kenji Taguchi (Eds.): Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings. Lecture Notes in Computer Science 7635, Springer 2012, ISBN 978-3-642-34280-6.

  • 組込みソフトウェア開発技術, 9章 組込みソフトウェアの静的検証技術 (pp.271-307), CQ出版, ISBN 978-4-7898-4548-9, 2011.

  • 電子情報通信学会 「知識ベース」, UML/ステートチャート, 7群1編2章5節(pp.35-44), 2009.

  • 吉岡信和,青木利晃,田原康之:SPINによる設計モデル検証,近代科学社,2008.

  • J.Gustafsson, T.Aoki and I.Lee(Editors): Proceedings of The Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, ISBN 0-7695-2124-X, IEEE Computer Society, 2004.

国内会議(査読付き)

  • 冨田尭,石井大輔,村上徹,竹内成樹,青木利晃: 大規模複雑Simulinkモデルのた めのMonte-Carlo最適化に基づいたテスト自動生成ツール,情報処理学会 組込みシ ステム研究会 組込みシステムシンポジウム,8 pages, 2018.

  • 青木利晃,千葉勇輝,松原正裕,成沢文雄: ISO26262のための安全要求記述言語と 追跡可能性検証手法の提案, プログラミングおよびプログラミング言語ワークショッ プ(PPL), 14 pages, 2016.

  • 青木利晃,トライチャイヤポーンクリアンクライ,千葉勇輝,松原正裕,西 昌能,成沢文雄:ゴール木とパターンを用いたISO26262における安全要求のモデル 化,組込みシステムシンポジウム, 2015.

  • 小川秀人, 市井誠, 粂野文洋, 青木利晃: POM/MCを用いた仮説ベースモデル検 査デバッグ手法,ソフトウェア工学の基礎ワークショップ, 日本ソフトウェア科学会, pp.137-142, 2013.

  • 陳適, 青木利晃:モデル検査ツールにより出力された反例に基づく誤り特定手法 ,ソフトウェア工学の基礎ワークショップ, 日本ソフトウェア科学会, p.27-p.32, 2012.

  • 青木利晃, 佐藤信, 谷充弘, 矢竹健朗: モデル検査とテストによる車載オペレー ティングシステムのシームレスな検証, 組込みシステムシンポジウム, pp.178-187, 2012.

  • 鈴木正人, 矢竹健朗, 青木利晃, 落水浩一郎: PBL形式による組込みシステム開発演習教育 -開発プロセスの発見と品質特性の実現-, 組込みシステムシンポジウム, 2011.

  • 西原秀明, 青木利晃, 粂野文洋, 篠崎孝一, 田口研治, 早水公二: MCBOK2008:ソフトウェア開発のためのモデル検査知識体系, 組込みシステムシンポジウム, pp.49-57, 2009.

  • 矢竹健朗, 西端浩和, 青木利晃: 環境モデリングによるモデル検査スクリプトの自動生成, 組込みシステムシンポジウム, pp.59-64, 2009.

  • 土肥雅俊, 青木利晃:Cプログラムの実行に基づいたモデル検査実験, ソフトウェア 工学の基礎ワークショップ, p.87-92, 2008.

  • 青木利晃, 山崎真吾: モデル検査によるリアルタイムオペレーティングシステムの設計検証, 組込みシステムシンポジウム, pp.159-166, 2008.

  • 青木利晃,関口正,平山雅之,岸知二:マルチタスクソフトウェアにおけるタスク 間状態不一致問題の検出と解析,情報処理学会 組込みシステム研究会 組込みシス テムシンポジウム, p.102-110, 2007.

  • 青木利晃,片山卓也:ステートチャートに基づいたオブジェクト指向設計モデルの 検証,ソフトウェア工学の基礎ワークショップ, p.55-64, 2005.

  • 青木利晃,片山卓也:RTOSに基づいたソフトウェアのためのモデル検査ライブラリ, 組込みソフトウェアシンポジウム, p.56-63, 2005.

  • 青木利晃,岸知二,片山卓也:センサーのモデル化とモデル検査技術の適用につい て,組込みソフトウェアシンポジウム, p.118-125, 2004.

  • 青木利晃,片山卓也:SPINを用いたオブジェクト指向分析モデルのデータフロー解 析手法,ソフトウェア工学の基礎ワークショップ, 日本ソフトウェア科学会, p.9-20, 2003.

  • 岡崎光隆,青木利晃,片山卓也:並行動作するオブジェクトからの処理列の抽出法, ソフトウェア工学の基礎ワークショップ, 日本ソフトウェア科学会, p.147-150, 2001.

  • 立石 孝彰, 青木利晃, 片山卓也: HOLを用いたオブジェクト指向分析モデルの検証, ソフトウェア工学の基礎ワークショップ, 日本ソフトウェア科学会, p.117-124, 2000.

  • 青木利晃, 片山卓也: オブジェクト指向組み込みシステム開発のための設計モデル SESモデル, ソフトウェア工学の基礎ワークショップ, 日本ソフトウェア科学会, p.157-p.164, 2000.

  • 青木利晃: ソフトウェア開発における各工程の対応づけ -組み込みシステム開発に 焦点をあてて-, ソフトウェアシンポジウム2000, ソフトウェア技術者協会, p.229-235, 2000.

  • 青木利晃, 片山卓也: オブジェクト指向分析モデルのプロトタイプ実行環境, オブ ジェクト指向シンポジウム'99, 情報処理学会, p.161-168, 1999.

  • 青木利晃, 片山卓也: モデルの一貫性検証のための公理系, ソフトウェア工学の基 礎ワークショップ, p.178-181, 1996.

  • 青木利晃, 片山卓也: オブジェクト指向方法論のための形式的モデル, 情報処理学 会オブジェクト指向シンポジウム, p.25-32, 1996.

国内会議(査読なし)

  • 武井優己, 青木利晃: VARモデルによるOSSプロジェクト同士が生存性に与える影響の分析, 第216回ソフトウェア工学研究発表会 情報処理学会,8 pages, 2024.

  • 青木利晃,冨田尭,河井達治,川上大介,千田伸男: 自動運転システムを対象としたシナリオ開発のためのモデリング言語,情報処理学会 ソフトウェア工学研究会 ソフトウェアエンジニアリングシンポジウム,pp.123-130, 2022.

  • 鈴木玄貴,冨田尭,青木利晃,河井達治,川上大介,千田伸男:自動運転システム開発におけるシミュレーション検証のためのテストケース作成手法の提案, 第207回ソフトウェア工学研究発表会 情報処理学会,8 pages, Vol.2021-SE-207(39),2021.

  • 田中健人,青木利晃,川上大介,千田伸男,河井達治,冨田尭:自動運転システム における画像を対象とした形式仕様記述言語BBSLの提案,情報処理学会 第205回ソ フトウェア工学研究発表会, pp.1-8, Vol.2020-SE-205,No.8,2020.

  • 太田十字光, 青木利晃: Event-Bに基づいた鉄道システムの実践的な形式化と検証,情 報処理学会 第203回ソフトウェア工学研究会, Vol. 2019-SE-203, No. 6, 8 pages, 2019.

  • 青木利晃,川上大介,千田伸男,冨田尭: 確率統計に基づいた故障木とテストによ る機械学習システムの系統的評価手法, 情報処理学会 ソフトウェア工学研究会 ソ フトウェアエンジニアリングシンポジウム,8 pages,2018.

  • 冨田尭, 石井大輔, 村上徹, 竹内成樹, 青木利晃. 大規模複雑Simulink モデルの ためのMonte-Carlo 最適化に基づいたテスト自動生成ツール. 組込みシステムシン ポジウム, 2018. (8 pages).

  • 藤田健治,青木利晃,平石邦彦:複合的因果関係分析手法を用いた遠隔診療の定量 的安全性評価,システム数理と応用研究会,6 pages, 2017.

  • 太田十字光, 田辺良則, 青木利晃: Java Pathfinder における弱公平性条件 の実装, 日本ソフトウェア科学会第33回全国大会,9 pages, 2016.

  • 藤田健治,青木利晃:遠隔診療におけるリスクアセスメント手法の提案, 情報処理 学会 第38回組込みシステム研究発表会(SIGEMB), 2015.

  • 立岡真人, 青木利晃, 金子峰雄: 再利用のためのRTLからの関数コード生成手法, 電子情報通信学会 VLSI設計技術研究会(VLD), 信学技報, vol.113, no.454, VLD2013-165, pp.171-176, 2014.

  • 陳適, 青木利晃:モデル検査器により出力された反例に基づく誤り特定に関する研 究, 情報処理学会 第177回ソフトウェア工学研究会, 2012.

  • 谷崎裕明, 青木利晃, 片山卓也: Alloyを用いた構成変更支援ツールと適用実験, 情報処理学会 第169回ソフトウェア工学研究会, 2010.

  • 青木利晃: 形式手法教育の取り組みについて, 先端ソフトウェア工学に関する Grace国際シンポジウム 形式手法の産業応用ワークショップ2010, pp.59-60.

  • 青木利晃, NGUYEN Tam Thi Minh:モデル検査による設計検証と整合テスト, 情報処 理学会 第14回組込みシステム研究会, 2009.

  • 青木利晃:モデル検査によるリアルタイムオペレーティングシステムの検証実験, 情報処理学会 全国大会, p.5-317-318, 2008.

  • 青木利晃:リアルタイムオペレーティングシステムの検証について, 情報処理学会 ソフトウェア工学研究会 ウィンターワークショップ,2008.

  • 岸知二,野中誠,青木利晃,吉村健太郎,野田夏子:第11回ソフトウェアプロダク トライン国際会議(SPLC2007)参加報告,情報処理学会 ソフトウェア工学研究会, 2007.

  • 沢田篤史,青木利晃,冨山宏之,久保秋真:組込みシステムシンポジウム2006実施 報告,組込みシステム研究会, 2007.

  • 沢田篤史,青木利晃,福安直樹,妻木俊彦,中村友昭,浦本直彦,羽生田栄一,鷲 崎弘宜,松塚貴英:ウィンターワークショップ2007・イン・那覇報告,情報処理学 会 ソフトウェア工学研究会,2007.

  • 青木利晃:周期イベントに基づいた並行タスクの振る舞いの検証法,情報処理学会 ソフトウェア工学研究会 ウィンターワークショップ,p.7-8, 2007.

  • 青木利晃:モデル検査ツールを用いた状態遷移図の検証について,情報処理学会ソ フトウェア工学研究会 ウィンターワークショップ,p.3-4, 2006.

  • 青木利晃,片山卓也:アクション言語と制約言語を用いて記述されたオブジェクト 指向設計モデルの検証法,日本ソフトウェア科学会 第2回ディペンダブルソフト ウェア研究会, p.61-70, 2005.

  • 青木利晃:オブジェクト指向分析・設計モデルの解析手法,ソフトウェア工学の基 礎ワークショップ, 日本ソフトウェア科学会, p.233-234, 2004.

  • 青木利晃,岸知二,片山卓也: 定理証明システムとモデル検査ツールを併用した設 計モデルの検証実験, 日本ソフトウェア科学会 第1回ディペンダブルソフトウェ ア研究会, p.49-58, 2004.

  • 青木利晃: オブジェクト指向モデルのための検証ツールの実装について, 情報処理 学会 ソフトウェア工学研究会 ウィンターワークショップ, p.7-8, 2004.

  • 青木利晃: 組み込みシステム開発への形式的手法の適用,組込みソフトウェアシン ポジウム2003, p.126-127, 2003.

  • 青木利晃,岸知二,中島震,河野真治,友部実,田村直樹:組み込みシステム開発 における最先端ソフトウェア基盤技術,組込みソフトウェアシンポジウム2003, p.117-123, 2003.

  • 青木利晃,片山卓也:状態遷移図の段階的構築のための論理的基盤, 情報処理学会 ソフトウェア工学研究会 研究報告 2003-SE-143,p.21-28,2003.

  • 岡崎光隆,青木利晃,片山卓也:並行オブジェクトモデルから並行スレッドモデル への変換法,情報処理学会 ソフトウェア工学研究会 研究報告 2003-SE-140, p.39-46,2003.

  • 青木利晃,片山卓也:オブジェクト指向分析モデルの検証について,情報処理学会 ソフトウェア工学研究会 ウィンターワークショップ, p.13-14, 2003.

  • 青木利晃,片山卓也: オブジェクト指向分析モデルの検証支援環境, 第19回 日本ソフトウェア科学会 全国大会論文集(CD-ROM), 2002.

  • 矢竹健朗,青木利晃,片山卓也:定理証明システムHOLにおけるオブジェクト指向 理論の構築,情報処理学会 ソフトウェア工学研究会 研究報告 2002-SE-138, p.19-26, 2002.

  • 岡崎光隆,青木利晃,片山卓也:組み込みシステム設計における並行正規表現を用 いたスレッドの抽出法,情報処理学会 ソフトウェア工学研究会 研究報告 2002-SE-138, p.35--42,2002.

  • 青木利晃: APSEC2002参加報告,情報処理学会 ソフトウェア工学研究会 研究報告 2002-SE-138, p.67-71, 2002.

  • 青木利晃: 組み込みシステムの動向,情報処理学会 ソフトウェア工学研究会 研究 報告 2002-SE-137, p.61-64, 2002.

  • 青木利晃, 片山卓也: オブジェクト指向組み込みシステム開発における科学的手法 の適用,情報処理学会 ソフトウェア工学研究会 ウィンターワークショップ, p.1-2, 2002.

  • 青木利晃, 片山卓也: SESアプローチへのスケジューリング理論の導入に関する考 察, 情報処理学会 ソフトウェア工学研究会 ウィンターワークショップ, p.9-10, 2001.

  • 岡崎光隆, 青木利晃, 片山卓也: 並行動作するオブジェクトからの処理列の抽出法, 情報処理学会 ソフトウェア工学研究会 研究報告 2000-SE-129, p.65-72, 2000.

  • 立石 孝彰, 青木 利晃, 片山 卓也: オブジェクト指向分析モデルの検証と公理系 の提案, ソフトウェア工学研究会 研究報告 2000-SE-127, 情報処理学会, p.39-45, 2000.

  • 青木利晃, 森本大喜, 片山卓也: オブジェクト指向設計モデルSES-Modelに基づい たソフトウェアの構成法, 情報処理学会 ソフトウェア工学研究会 サマーワーク ショップ, p.57-58, 1999.

  • 花田真樹, 青木利晃, 片山卓也: オブジェクト指向方法論のための検証フレームワー クに関する研究, ソフトウェア工学研究会 研究報告 99-SE-122, 情報処理学会, p.101-108, 1999.

  • 青木利晃, 内藤壮司, 片山卓也: 組み込みシステムを対象とした設計手法の形式化, 情報処理学会 ソフトウェア工学研究会ウィンターワークショップ, p.3-4, 1999.

  • 青木利晃, 内藤壮司, 片山卓也: オブジェクト指向組み込みシステム開発のための Ses-Basedアプローチ, 第15回全国大会論文集, 日本ソフトウェア科学会, p.289-292, 1998.

  • 石田至, 青木利晃, 片山卓也: オブジェクト指向方法論のための形式的モデルの検 証, ソフトウェア工学研究会 研究報告 98-SE-118, 情報処理学会, p.135-141, 1998.

  • 青木利晃, 古川順一, 片山卓也: 形式的オブジェクト指向方法論FO∀Mの構築法と その支援環境ソフトウェア工学研究会 研究報告 98-SE-118, 情報処理学会, p.143-150, 1998.

  • 青木利晃, 片山卓也: 複数視点からのシステムモデリングにおけるモデル統合と形 式的手法, In 情報処理学会 ソフトウェア工学研究会 ウィンターワークショップ, p.9-10, 1998.

  • 青木利晃, 石田至, 古川順一, 片山卓也: オブジェクト指向分析モデルにおける一 貫性検証のための公理系の実装, 第14回全国大会論文集, 日本ソフトウェア科学会, p.465-468, 1997.

テクニカルレポート

  • Yuki Yamaguchi, Toshiaki Aoki: Attack Tree Analysis for Adversarial Evasion Attacks. CoRR abs/2312.16957, 2023.

  • Toshiaki Aoki, Aritoshi Hata, Kazusato Kanamori, Satoshi Tanaka, Yuta Kawamoto, Yasuhiro Tanase, Masumi Imai, Fumiya Shigemitsu, Masaki Gondo, Tomoji Kishi: Model-Checking in the Loop Model-Based Testing for Automotive Operating Systems. CoRR abs/2310.00973, 2023.

  • Toshiaki Aoki, Makoto Satoh, Mitsuhiro Tani, Kenro Yatake and Tomoji Kishi: Combined Model Checking and Testing Create Confidence in Correctness of Commercial Automotive Operating System, Research Report, School of Information Science, Japan Advanced Institute of Science and Technology, IS-RR-2016-002, 2016.

  • Kenro Yatake, Hirokazu Nishibata and Toshiaki Aoki: Automatic Generation of Model Checking Scripts based on Environment Modeling, Research report, School of Information Science, Japan Advanced Institute of Science and Technology, IS-RR-2010-001, 2010.

  • 西原秀明、青木利晃、粂野文洋、篠崎孝一、田口研治、早水公二: MCBOK2008:ソフトウェア開発のためのモデル検査知識体系, 産業技術総合研究所 テクニカルレポー ト,PS-2009-009, 2009.

  • Hideaki Nishihara, Koichi Shinozaki, Koji Hayamizu, Toshiaki Aoki, Kenji Taguchi, Fumihiro Kumeno:Model checking education for software engineers in Japan (Preliminary Version),産業技術総合研究所 テクニカルレポート, PS-2008-013, 2008.

  • 青木利晃、粂野文洋、木下佳樹、篠崎孝一、高木理、高村博紀、田口研治、中原早 生、西原秀明、早水公二、本位田真一、渡邊宏:モデル検査の教育プログラム構築に向けて,産業技術総合研究所 テクニカルレポート,PS-2008-013, 2008.

口頭発表

  • 青木利晃,千葉勇輝,小川直哉:モデル検査ツールにより出力された反例に基づく誤り特定に関する研究, プログラム・デバッグ自動化の現状と今後, ソフトウェ アエンジニアリングシンポジウム ワークショップ, 2013.

  • Toshiaki Aoki:Verification of Real-Time Operating System with Model Checking, 57th IFIP WG 10.4 Meeting, Jan.23, 2010.

  • 青木利晃:形式手法の概要とモデル検査, 第13回組込みシステム技術展, 2010.

  • 青木利晃:RTOS設計検証の経験から,ソフトウェアシンポジウム2010 WG3:形式手 法モデリング, 2010.

  • 青木利晃:形式手法概論, 第11回組込みシステム技術展, 2008.

  • 早水公二, 青木利晃, 粂野文洋, 木下佳樹, 篠崎孝一, 田口研治, 中原早生, 西原 秀明, 本位田真一: モデル検査の教育プログラムの構築に向けて, システム検証の科学, 2008(口頭発表).

  • 青木利晃:マルチタスクソフトウェアの検証法, JAIST 21st Century COE Symposium 'Verifiable and Evolvable e-Society', Sep.6th, 2007.

  • 青木利晃:モデル検査手法の普及に関する取り組み, JAIST 21st Century COE Symposium 'Verifiable and Evolvable e-Society', Sep.6th, 2007.

  • Toshiaki Aoki:Applying Theorem Proving System to Verification of Object-Oriented Design Model, JAIST-Chalmers-AIST Workshop, May 19th, 2006.

調査報告

  • 高田広章,青木利晃,飯山真一,石濱直樹,岸田昌巳,高橋孝一,西康晴,門田浩: 組込みシステム関連技術の動向等に関する調査研究, 機械産業等の産業活動に関する調査研究 15-II-1-001, 財団法人 産業技術研究所 (委託先 財団法人ソフトウェア工学研究財団), 2003.

  • 鈴木正人,青木利晃,丸山勝久,鷲崎弘宜,青山幹雄: コンポーネントウェア技術の確立に関する調査研究, 機械産業等の産業活動に関する調査研究 14-II-2-001, 財団法人 産業技術研究所 (委託先 財団法人ソフトウェア工学研究財団), 2003.

  • 片山卓也,鯵坂恒夫,岸知二,鈴木正人,青木利晃,小倉晴美:ソフトウェア工学 の戦略的推進に関する調査研究,機械産業等の産業活動に関する調査研究 13-1, 財団法人 産業技術研究所(委託先財団法人ソフトウェア工学研究財団), 2002.

その他

  • Jaejoon Lee, Isabel John, Toshiaki Aoki, John D. McGregor: SPLC 2007 Dectoral Symposium. SPLC (2)p.155-156, 2007.

招待講演

  • 車載システム開発における形式手法実践の現状と課題, 招待講演,日本ソフトウェア科学会 第16回 ディペンダブルシステムワークショップ(DSW 2018).

  • 形式手法と安全性,招待講演,安全工学会 安全工学研究発表会 2018.

  • Vehicles need Formal Methods: the 19th National Symposium of Selected ICT Problems, Hanoi, invited talk, Oct. 1-2, 2016.

  • 車載ソフトウェアの安全性:現状と課題, 第1回 日本情報科教育学会 関東・東北 支部大会, 招待講演, 2014/3/22.

  • 形式手法の研究と実践からざっくばらんに…~産業界での可能性や今後の展 望~,フォーマルメソッド普及促進セミナー2011 in 札幌,基調講演, 2011/7/22.

  • モデル検査手法の普及活動とその応用,SPI Japan 2009, 2009/10/6

  • 実用的な形式手法 - モデル検査手法とその応用, 東芝ソフトウェアフォーラム 2009/第九回東芝SEPGカンファレンス, 2009/7/10

  • 組込みソフトウェアの形式検証の現状と課題,情報処理学会 デザインガイア, 2006/11/29

  • 定理証明システムとソフトウェアの検証への応用, システム設計検証技術研究会, 2005/4/25.

  • ソフトウェアと検証技法, 自然科学重点研究集会, 2005/2/3.

チュートリアル

  • ソフトウェアモデル検査入門: 北陸先端科学技術大学院大学/日本科学技術連盟, 2008 9/29-10/1

  • ソフトウェアモデル検査入門: 北陸先端科学技術大学院大学/日本科学技術連盟, 2007 12/10-12

  • ソフトウェアモデル検査入門: 北陸先端科学技術大学院大学/日本科学技術連盟, 2007 1/16-18

  • モデル検査技術入門: 情報処理推進機構 ソフトウェアエンジニアリングセンター, 2006/10/30

  • ソフトウェアモデル検査入門: 北陸先端科学技術大学院大学/日本科学技術連盟, 2006 5/30-6/1

  • 検証技術-モデル検査と定理証明-, 情報処理学会 連続セミナー2005

  • 組込みソフトウェアの検証:組込みシステム技術に関するサマーワークショップ, 2005

  • 組込みソフトウェア検査・検証:北陸IT総合人材育成センター,2005