研究者情報 - 木下　佳樹

（最終更新日：2022-12-09 16:58:36）

  キノシタ　ヨシキ   Kinoshita Yoshiki
  木下　佳樹
   所属   神奈川大学情報学部計算機科学科

神奈川大学大学院理学研究科理学専攻（情報科学領域）

職種教授

■ 専門分野

ソフトウェア科学, プログラム意味論　（キーワード：プログラム意味論(算譜意味論)、プログラミング科学、算譜検証論）

■ 学歴・学位

1.	1986/04～1989/03	東京大学大学院理学系研究科情報科学専攻博士課程修了
2.	1984/04～1986/03	東京大学大学院理学系研究科情報科学専攻修士課程修了
3.	1983/04～1984/03	東京大学理学部情報科学科研究生
4.	1976/04～1981/03	東京大学教養学部理科一類卒業理学士

■ 学位等

理学博士

■ 著書・論文歴

1.	論文	A Modelling Approach for System Life Cycles Assurance Springer Lecture Notes in Computer Science 11699,pp.16-27 （共著） 2019/09
2.	論文	A Thought Experiment on Evolution of Assurance Cases - from a Logical Aspect Springer Lecture Notes in Computer Science (10489),pp.17-26 （共著） 2019/09
3.	論文	開放系総合信頼性の新標準IEC62853の概要と意義標準化と品質管理 72(5),42-44頁（共著） 2019/05
4.	論文	開放系総合信頼性の標準化〜CREST研究プロジェクトとIEC標準化の相互作用〜デジタルプラクティス 10(1) （共著） 2019/01
5.	論文	IEC 62856 Open systems dependability の背景と今後～合意形成，説明責任，障害対応，変化対応～信学技報 117(355),19-23頁（共著） 2017/12
6.	論文	Category theoretic structure of setoids Theoretical Computer Science (Elsevier) 546,pp.145-163 （共著） 2014/08
7.	その他	Argument for Agreement and Assurance (AAA) LNAI, New Frontiers in Artificial Intelligence, JSAI-isAI 2013 Workshops 8417,pp.XIV-XIV （共著） 2014/04
8.	著書	Assurance Case as a Proof in a Theory: towards Formulation of Rebuttals, in "Assuring the Safety of Systems, Proceedings of the Twenty-first Safety-Critical Systems Symposium, Bristol, UK, 5-7th February 2013" 205-230頁（共著） 2013/03
9.	論文	帰納と再帰ー表示的意味論の第一歩『コンピュータソフトウェア』（岩波書店） 29(1),30-46頁（単著） 2012/01
10.	論文	Using a Proof Assistant to Construct Assurance Cases Corectness by Construction (Fast Abstract) Proceedings of the 42nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2012) （共著） 2012
11.	論文	A Coalgebraic Approach to Supervisory Control of Partially Observed Mealy Automata Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO2011(Springer-Verlag) LNCS,6859,253-267頁（共著） 2011
12.	論文	A design for an assessment procedure for dependability based on a formal model, in "Proceedings of The Second IASTED International Conference on Advances in Management Science and Risk Assessment (AMSRA2010)" （共著） 2010/11
13.	論文	記述の科学　第3回　記述の構成と利用『情報処理』（情報処理学会） 51(10),1332-1340頁（共著） 2010/10
14.	論文	記述の科学　第2回　視点と形式的体系『情報処理』（情報処理学会） 51(9),1204-1214頁（共著） 2010/09
15.	論文	記述の科学　第1回　記述とは、『情報処理』（情報処理学会） 51(8),1049-1057頁（共著） 2010/08
16.	その他	オープンシステムディペンダビリティと利用者指向～課題と解決へのアプローチ～『第8回ディペンダブルシステムワークショップ予稿集』日本ソフトウェア科学会（共著） 2010/07
17.	論文	A field-scientific approach to Clinico-Informatics Synthesiology (National Institute of Advanced Industrial Science and Technology) 3(1),64-76頁（共著） 2010/07
18.	論文	臨床情報学のための野外科学的方法ー技術移転の方法論に向けて『シンセシオロジー』（産業技術総合研究所） 3(1),36-46頁（共著） 2010/03
19.	論文	Agate-an Agda-to-Haskell compiler Computer Software (Iwanami shoten) 26(4),107-119頁（共著） 2009/11
20.	著書	A simple type-theoretic language: Mini-TT 139-164頁（共著） 2009/09
21.	その他	User Oriented Dependability 『第7回ディペンダブルシステムワークショップ予稿集』日本ソフトウェア科学会（単著） 2009/07
22.	その他	Formalization of System LSI Specification and Automatic Generation of Verification Items 『算譜科学研究速報』（産業技術総合研究所） PS-2009-006 （共著） 2009/07
23.	論文	An algebraic semantics of predicate abstraction for PML Computer Software (Iwanami shoten) 26(2),147-156頁（共著） 2009/04
24.	その他	Fieldwork and the 4:6 Principle-Introduction to the Research Center for Verification and Semantics, in "Proceedings of IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, 2009. ISORC '09" IEEE Computer Society http://ieeexplore.ieee.org/頁（単著） 2009/03
25.	その他	Agda言語について『日本ソフトウェア科学会第25回大会予稿集』（日本ソフトウェア科学会）（共著） 2008/09
26.	その他	モデル検査の教育プログラム構築に向けて算譜科学研究速報（産業技術総合研究所） PS-2008-012 （共著） 2008/08
27.	その他	書類の定式化と検証第6回ディペンダブルシステムワークショップ予稿集（日本ソフトウェア科学会）（単著） 2008/07
28.	論文	フォーマルメソッドのフィールドワーク『情報処理』（情報処理学会） 49(5),499-505頁（共著） 2008/05
29.	その他	型理論での形式的証明記述の技法について日本ソフトウェア科学会第22回大会予稿集（共著） 2005/09
30.	論文	Improvement on Integrity Checking System for Software in Weighing Instrument (電子出版) （共著） 2005
31.	論文	テスト付クリーニ代数の準代数構造『コンピュータソフトウェア』（岩波書店） 20(2),47-53頁（共著） 2003/03
32.	論文	Essentially algebraic structure for Kleene algebra with tests and its application to semantics of while programs IPSJ Transactions on Programming (Information Processing Society of Japan) 44(SIG 4(PRO 17)),47-53頁（共著） 2003/03
33.	その他	A Functorial Approach to Refinement AIST Programing Science Group Technical Report AIST-PS-2001-01,49-63頁（共著） 2001/04
34.	論文	Data Refinement and algebraic structure Acta Informatica (Springer-Verlag) 36(9 and 10),693-719頁（共著） 2000/04
35.	論文	A general completeness result in refinement , in "Recent Trends in Algebraic Development Techniques" (eds. Didier Bert, Christine Choppy and Peter D. Mosses) (Springer-Verlag) 1827,201-218頁（共著） 2000
36.	論文	Sketches Journal of Pure and Applied Algebra (Elsevier) 143,275-291頁（共著） 1999/11
37.	論文	Proving Through Commutative Diagrams, in "Logic, Language and Computation, volume 2" (eds. Lawrence S. Moss, Jonathan Ginzburg, and Maarten de Rijke) CSLI Lecture Notes (University of Chicago Press) 96,128-142頁（共著） 1999/04
38.	その他	ソフトウェアの複雑さ『Computer Today』（サイエンス社） 15(3),18-22頁（単著） 1998/05
39.	論文	クヌース・ベンディクスの代わりに米田ーモノイドの場合『コンピュータソフトウェア』（岩波書店） 16(2),72-75頁（単著） 1998/04
40.	論文	A bicategorical analysis of E-categories Mathematica Japonicae (International Society for Mathematical Sciences) 47(1),157-169頁（単著） 1998/01
41.	論文	An axiomatic approach to binary logical relations with applications to data refinement Lecture Notes in Computer Science (Springer-Verlag) 1281,191-212頁（共著） 1997/09
42.	論文	証明支援系の図式によるインターフェイス『コンピュータソフトウェア』（岩波書店） 14(3),42-50頁（共著） 1997/05
43.	その他	Groupoid of Equational Proofs 『電子技術総合研究所彙報』（オーム社） 60(1),711-718頁（共著） 1996/11
44.	論文	Lax naturality through enrichment Journal of Pure and Applied Algebra (Elsevier) 112(1),53-72頁（共著） 1996/10
45.	論文	Data Refinement for Call-By-Value Programming Lanuages Lecture Notes in Computer Science (Springer-Verlag) 1683,562-576頁（共著） 1996/10
46.	その他	ソフトウェアの差分「協調プログラミング例題集「文殊の知恵」を目指して」、bit別冊、共立出版 51-60頁（単著） 1996/04
47.	論文	A fibrational semantics of logic programs, in "Extensions of Logic Programming, 5th International Workshop, ELP'96, Leipzig, Germany" Extensions of Logic Programming, 5th International Workshop, ELP'96, Leipzig, Germany (Springer-Verlag) 1050,177-192頁（共著） 1996/03
5件表示
全件表示(47件)

■ 所属学会

1.	2002/04～	情報処理学会
2.	1987/10～	日本ソフトウェア科学会

■ 研究課題・受託研究・科研費

1.	2018/09～2019/12	Towards Identifying and closing Gaps in Assurance of autonomous Road vehicleS (TIGARS) 競争的資金等の外部資金による研究（キーワード：assurance, dependability, autonomous system）
2.		平塚市地域防災計画の整合性検査方式の研究国内共同研究
3.	2008/10～2014/03	利用者指向ディペンダビリティの研究競争的資金等の外部資金による研究（キーワード：ディペンダビリティ、規格、オープンシステム）
4.	2014/06～2016/02	オープンシステム・ディペンダビリティのための形式アシュランスケース・フレームワーク競争的資金等の外部資金による研究（キーワード：アシュランスケース、形式アシュランスケース、ディペンダビリティ、オープンシステム・ディペンダビリティ）
5.	2016/04～	開放系総合信頼性の研究個人研究
6.	2012/04～2014/03	議論の枠組みに関する基礎理論および応用に関する研究国内共同研究
5件表示
全件表示(6件)

■ 講師・講演

1.	2019/07	ディペンダビリティ標準の新しい動向〜新国際標準IEC 62853がもたらすもの（東京）
2.	2018/12	IEC 62853 Open systems dependability について（東京）
3.	2016/09	オープンシステム・ディペンダビリティのアシュランス議論とディペンダビリティケース（東京）
4.	2014/06	妥当性確認とアシュランスケース(独)科学技術振興機構　研究開発戦略センター　システム科学ユニット　第8回システム科学検討会（東京）

■ 委員会・協会等

1.	2004/04～2008/03	日本ソフトウェア科学会理事
2.	2008/12～	情報処理学会　情報規格調査会　ISO/IEC JTC1 Information technology SC7 Systems and software engineering WG7 Life cycle management 国内小委員会委員
3.	2010/04～	日本規格協会 IEC TC56 Dependability WG4 System aspects of dependability 国内小委員会委員
4.	2014/04～	IEC TC56 ディペンダビリティ国内委員会 WG4 情報システム主査
5.	2012/10～	IEC TC56 Dependability WG4 System aspects of dependability Convenor
6.	2013/01～2018/06	IEC TC56 Dependability PT 4.8 Open Systems Dependability Project leader
7.	2011/10～	Liaison from IEC TC56 Dependability to ISO/IEC JTC1 Information technology SC7 Systems and software engineering Liaison officer
8.	2012/10～	Liaison from ISO/IEC JTC1 Information Technology SC7 Software Engineering to IEC TC56 Dependability Liaison officer
9.	2016/06～2019/03	ISO/IEC JTC 1/SC 7/WG 7 Project leader, ISO/IEC/IEEE 15026-1 Systems and software assurance Part 1: Concepts and vocabulary
10.	2016/06～	ISO/IEC JTC 1/SC 7/WG 7 Project leader, ISO/IEC/IEEE 15026-2 Systems and software assurance Part 2: Assurance case
11.	2016/06～	ISO/IEC JTC 1/SC 7/WG 7 Project leader, ISO/IEC/IEEE15026 Systems and software assurance Part 4: Assurance in the life cycle
12.	2014/02～	一般社団法人ディペンダビリティ技術推進協会標準化部会主査
13.	2018/06～	一般社団法人　ディペンダビリティ技術推進協会理事
5件表示
全件表示(13件)

■ メールアドレス

■ 受賞学術賞

1.	2018/09	International Electrotechnical Commission (IEC) IEC 1906 award
2.	2012/05	国際規格開発賞

■ 取得特許

2014/12/12

整合性検査装置、整合性検査方法、及びプログラム（特許第5660503号）

■ 研究経歴

1.	1996 2005 文部科学省　中核的研究拠点（COE）育成：大域情報処理技術
2.	2002 2008 検証における記述量爆発問題の構造変換による解決、科学技術振興機構CREST制度、「情報社会を支える新しい高性能情報処理技術」研究領域 Solving the Description Explosion Problem in System Verification through Structural Transformation, conducted as a project of JST CREST, New High-Performance Information Processing Technology Supporting Information-Oriented Society - Aiming at the Creation of New High-Speed, Large-Capacity Computing Technology Based on Quantum Effects, Molecular Functions, Parallel Processing" research domain"
3.	2008 2014 利用者指向ディペンダビリティの研究（科学技術振興機構CREST制度「実用化をめざした組込みシステム用ディペンダブル・オペレーティングシステム」研究領域） Study on user-oriented dependability, conducted as a project in JST CREST, Dependable Engineering for Open Systems research domain.
4.	2012 2014 議論の発展過程の数理科学的研究、国立情報科学研究所一般共同研究 Mathematical study on evolution processes of argument, Collaborative research project of NII
5.	2014 2016 オープンシステム・ディペンダビリティのための形式アシュランスケース・フレームワーク

■ 本学関連サイト

1.	「神大の先生」サイトページ