2024/09/17 更新

写真a

ユウエン　シヨウジ
結縁　祥治
YUEN, Shoji
所属
大学院情報学研究科 情報システム学専攻 ソフトウェア論 教授
大学院担当
大学院情報科学研究科
大学院情報学研究科
学部担当
工学部
情報学部 コンピュータ科学科
職名
教授
連絡先
メールアドレス
ホームページ
http://www.sqlab.jp/person/yuen/index.html

学位 2

  1. 博士(工学) （ 1997年2月   名古屋大学 ） 

  2. 工学修士 （ 1987年3月   京都大学 ） 

学位の先頭へ▲

研究分野 1

  1. その他 / その他  / 計算機科学

研究分野の先頭へ▲

現在の研究課題とSDGs 1

  1. 並行プログラムの形式的意味論

現在の研究課題とSDGsの先頭へ▲

経歴 5

  1. 名古屋大学   大学院情報学研究科   教授

    2007年4月 - 現在

    　 詳細を見る

    国名：日本国

  2. 名古屋大学   大学院情報科学研究科   准教授

    2003年4月 - 2007年3月

    　 詳細を見る

    国名：日本国

  3. 名古屋大学   工学研究科   助教授

    2000年8月 - 2003年3月

    　 詳細を見る

    国名：日本国

  4. 名古屋大学   情報メディア教育センター   助教授

    1998年4月 - 2000年7月

    　 詳細を見る

    国名：日本国

  5. 名古屋大学   工学部   助手

    1990年4月 - 1998年3月

    　 詳細を見る

    国名：日本国

経歴の先頭へ▲

学歴 3

  1. 名古屋大学   工学研究科   情報工学

    1987年4月 - 1990年3月

    　 詳細を見る

    国名： 日本国

  2. 京都大学   工学研究科   情報工学専攻

    1985年4月 - 1987年3月

    　 詳細を見る

    国名： 日本国

  3. 京都大学   工学部   情報工学科

    - 1985年

    　 詳細を見る

    国名： 日本国

学歴の先頭へ▲

所属学協会 5

  1. 電子情報通信学会   研究専門委員会委員長(ソフトウェアサイエンス)

    2014年5月 - 2016年4月

  2. 情報処理学会   東海支部評議員

    2009年5月 - 2011年4月

  3. 日本ソフトウェア科学会   学会誌編集委員

    2004年4月 - 2017年3月

  4. 情報処理学会   東海支部幹事

    2002年4月 - 2004年3月

  5. Association for Computer Machinary

所属学協会の先頭へ▲

委員歴 19

  1. 16th International Conference on Reversible Computation (RC)   Program Committee member  

    2023年11月 - 2024年7月   

    　 詳細を見る

    団体区分：学協会

  2. 20th International Conference on Formal Aspects of Component Software   Program Committee member  

    2024年3月 - 2024年11月   

    　 詳細を見る

    団体区分：学協会

  3. PLACES 2024: 15th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software   Program Committee member  

    2023年11月 - 2024年3月   

    　 詳細を見る

    団体区分：学協会

  4. 19th International Conference on Formal Aspects of Component Software   Program Committee member  

    2023年4月 - 2023年11月   

    　 詳細を見る

    団体区分：学協会

  5. Program Committee member  

    2022年9月 - 2023年3月   

    　 詳細を見る

    団体区分：学協会

  6. 18th international conference on Formal Aspects of Component Software   Program Committee member  

    2022年3月 - 2022年11月   

    　 詳細を見る

    団体区分：その他

  7. 15th International Conference, Reversible Comoputation   Program Committee member  

    2022年11月 - 2023年7月   

  8. 17th International Conference on Formal Aspects of Component Software   PCmember  

    2021年10月   

    　 詳細を見る

    団体区分：学協会

  9. 13th International Conference, Reversible Computing   General Chair  

    2020年8月 - 2021年7月   

    　 詳細を見る

    団体区分：学協会

  10. 16th International Conference on Formal Aspects of Component Software   PCmember  

    2019年10月   

    　 詳細を見る

    団体区分：学協会

  11. 13th International Colloquium on Theoretical Aspects of Computing   PCmember  

    2016年11月   

  12. 2014年日本ソフトウェア科学会大会   2014大会実行委員長  

    2014年1月 - 2014年9月   

    　 詳細を見る

    団体区分：学協会

  13. 11th International Symposium on Automated Technology for Verification and Analysis   PCmember  

    2013年10月   

  14. 23rd International Conference on Concurrency Theory   PCmember  

    2011年9月 - 2012年9月   

  15. Structural Operational Semantics 2008   PCmember  

    2008年9月   

  16. 6th International Symposium on Automated Technology for Verification and Analysis   PCmember  

    2008年9月   

  17. 8th International Symposium on Functional and Logic Programming   General Chair  

    2008年5月   

  18. Structural Operational Semantics 2007   PCmember  

    2007年9月   

    　 詳細を見る

    団体区分：学協会

  19. 5th International Symposium on Automated Technology for Verification and Analysis   PCmember  

    2007年9月   

▼全件表示

委員歴の先頭へ▲
 

論文 83

  1. Constant Propagation in CRIL by Bidirectional Data Flow Analysis 査読有り

    Snunya Oguchi, Shoji Yuen

    Journal of Information Processing   32 巻   頁： 552 - 564   2024年7月

    　詳細を見る

    担当区分：責任著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： https://doi.org/10.2197/ipsjjip.32.552

  2. Concurrent RSSA for CRIL: Flow Analysis for a Concurrent Reversible Programming Language 査読有り

    Shunya Oguchi, Shoji Yuen

    Lecture Notes in Computer Science   14680 巻   頁： 181 - 200   2024年5月

    　詳細を見る

    担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

    DOI： https://doi.org/10.1007/978-3-031-62076-8_12

  3. revTPL: The Reversible Temporal Process Language 査読有り 国際共著

    Laura Bocchi ; Ivan Lanese ; Claudio Antares Mezzina ; Shoji Yuen.

    Logical Method in Computer Science   20 巻 ( 1 ) 頁： 11:1 - 11:35   2024年1月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： https://doi.org/10.46298/lmcs-20(1:11)2024

  4. CRIL: A Concurrent Reversible Intermediate Language 査読有り

    Shunya Oguchi, Shoji Yuen

    Electronic Proceedings in Theoretical Computer Science   387 巻   頁： 149 - 167   2023年9月

    　詳細を見る

    担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

    DOI： https://dx.doi.org/10.4204/EPTCS.387.11

  5. 可逆並行オブジェクト指向プログラミング言語：CROOPLPP

    赤池佑介,結縁祥治

    信学技報   123 巻   頁： 13 - 18   2023年7月

    　詳細を見る

    担当区分：責任著者   記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）  

  6. CRSSA: 並行可逆言語に対する静的単一代入 査読有り

    小口隼也, 結縁祥治

    第25回プログラミングおよびプログラミング言語ワークショップ PPL 2023     頁： 1 - 20   2023年3月

    　詳細を見る

    担当区分：責任著者   記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）  

  7. A reversible debugger for imparative parallel programs with contracts 査読有り

    Takashi Ikeda, Shoji Yuen

    Reversible Computation 2022, Lecture Notes in Computer Science   13354 巻   頁： 204 - 212   2022年7月

    　詳細を見る

    担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

    DOI： https://doi.org/10.1007/978-3-031-09005-9_14

  8. The reversible temporal process language 査読有り 国際共著

    Laura Bocchi, Ivan Lanese, Claudio Antrares Mezzina, Shoji Yuen

    Proceedings of FORTE 2022, Lecture Notes in Computer Science   13273 巻   頁： 31 - 49   2022年6月

    　詳細を見る

    担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

    DOI： https://doi.org/10.1007/978-3-031-08679-3_3

  9. 再帰的ブロック構造を持つ並列プログラムに対する可逆実行環境 査読有り

    池田崇志，結縁祥治

    情報処理学会論文誌トランザクション     2021年11月

    　詳細を見る

    担当区分：責任著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  10. Multiparty Session Programming with Global Protocol Combinators(Artifact) 招待有り 査読有り 国際共著

    Keigo Imai, Rumiyana Neykova, Nobuko Yoshida, Shoji Yuen

    Dagstuhl Artifacts Series   6 巻 ( 2 ) 頁： 1 - 2   2020年11月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（その他学術会議資料等）  

    DOI： 10.4230/DARTS.6.2.18

  11. Multiparty Session Programming with Global Combinators 招待有り 査読有り 国際共著

    Keigo Imai, Rumiyana Neykova, Nobuko Yoshida, Shoji Yuen

    LIPlcs   166 巻   頁： 9:1 - 9:30   2020年11月

    　詳細を見る

    担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

    DOI： 10.4230/LIPIcs.ECOOP.2020.9

  12. A Reversible Runtime Environment for Parallel Programs 査読有り

    Takashi Ikeda, Shoji Yuen

    Reversible Computation 2020, Lecture Notes in Computer Science   12247 巻   頁： 272-279   2020年7月

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1007/978-3-030-52482-1_18

  13. Fault Diagnosis for Distributed Cooperative System Using Inducting Logic Programming 招待有り 査読有り

    Shuichi Sato, Yosuke Watanabe, Hiroyuki Seki, Yoshinao Ishii, Shoji Yuen

    IEEE International Conference on Prognostics and Health Management, ICPHM 2020     頁： 1 - 8   2020年6月

    　詳細を見る

    担当区分：責任著者  

    DOI： 10.1109/ICPHM49022.2020.9187032

  14. Automating Time-series Safety Analysis for Automotive Control Systems Using Weighted Partial Max-SMT 査読有り

    Shuichi Sato, Shogo Hattori, Hiroyuki Seki, Yutaka Inamori, Shoji Yuen

    Journal of Information Processing   28 巻   頁： 124-135   2020年1月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.2197/ipsjjip.28.124

  15. Session-ocaml: A session-based library with polarities and lenses 査読有り

    Keigo Imai, Nobuko Yoshida, Shoji Yuen

    Science of Computer Program   172 巻   頁： 135-159   2019年3月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1016/j.scico.2018.08.005

  16. Reversing Event Structure 査読有り

    Irek Ulidowski, Iain Phillips, Shoji Yuen

    New Generation Computing   36 巻   頁： 281-306   2018年9月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1007/s00354-018-0040-8

  17. Reversing Parallel Programs with Blocks and Procedures 査読有り

    James Hoey, Irek Ulidowski, Shoji Yuen

    EPTCS (EXPRESS/SOS 2018)   276 巻   頁： 69-86   2018年9月

    　詳細を見る

    記述言語：英語  

    DOI： 10.4204/EPTCS.276.7

  18. Nested Timed Automata with Invariants 査読有り

    Yuwei Wang, Guoqiang Li, Shoji Yuen

    Lecture Notes in Computer Science   10606 巻   頁： 77-93   2017年10月

    　詳細を見る

    記述言語：英語  

    DOI： 10.1007/978-3-319-69483-2

  19. Nested Timed Automata with Diagonal Constraints 査読有り

    Yuwei Wang, Yunqing Wen, Guoqiang Li, Shoji Yuen

    Lecture notes in computer science   10610 巻   頁： 396-412   2017年11月

    　詳細を見る

    記述言語：英語  

    DOI： 10.1007/978-3-319-68690-5_24

  20. Reversing Imperative Parallel Programs. 査読有り

    James Hoey, Irek Ulidowski, Shoji Yuen

    Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics and 14th Workshop on Structural Operational Semantics, EXPRESS/SOS 2017, Berlin, Germany, 4th September 2017. EPTCS 255, 2017     2017年9月

    　詳細を見る

    記述言語：英語  

    DOI： 10.4204/EPTCS.255.4

  21. Session-ocaml: A Session-Based Library with Polarities and Lenses 査読有り

    Keigo Imai, Nobuko Yoshida, Shoji Yuen

    Lecture Notes in Computer Science   10319 巻   頁： 99-118   2017年6月

    　詳細を見る

    記述言語：英語  

    DOI： 10.1007/978-3-319-59746-1_6

  22. Automating Time Series Safety Analysis for Automotive Control Systems in STPA Using Weighted Partial Max-SMT 査読有り

    Shuichi Sato, Shogo Hattori, Hiroyuki Seki,Yutaka Inamori,Shoji Yuen

    Communications in Computer and Information Science   ( 694 ) 頁： 39-54   2016年11月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1007/978-3-319-53946-1_3

  23. An Over-Approximation Forward Analysis for Nested Timed Automata 査読有り

    Yunqing Wen, Guoqiang Li, Shoji Yuen

    Lecture Notes in Computer Science   8979 巻   頁： 1-15   2015年1月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

  24. Nested Timed Automata with Frozen Clocks 査読有り

    Guoqiang Li, Mizuhito Ogawa, Shoji Yuen

    Lecture Notes in Computer Science   9268 巻   頁： 189-205   2015年9月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    A nested timed automaton (NeTA) is a pushdown system whose control locations and stack alphabet are
    timed automata (TAs). A control location describes a working TA, and the stack presents a pile of
    interrupted TAs. In NeTAs, all local clocks of TAs proceed uniformly also in the stack. This paper extends
    NeTAs with frozen local clocks (NeTA-Fs). All clocks of a TA in the stack can be either frozen or
    proceeding when it is pushed. A NeTA-F also allows global clocks adding to local clocks in the working
    TA, which can be referred and/or updated from the working TA. We investigate the reachability of NeTAFs
    showing that (1) the reachability with a single global clock is decidable, and (2) the reachability with
    multiple global clocks is undecidable.

  25. Concurrency and reversibility 招待有り 査読有り

    Irek Ulidowski, Iain Phillips and Shoji Yuen

    Reversible Computation 2014, LNCS 8507   ( 8507 ) 頁： 1-14   2014年7月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

  26. 値付きタスクオートマトンに基づくコストを意識した実時間タスクスケジューリング

    結縁祥冶、亀井達朗

    信学技報   114 巻 ( 127 ) 頁： 37-42   2014年7月

    　詳細を見る

    担当区分：筆頭著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  27. 離散事象システムにおけるMaxSATソルバを用いた最大可制御部分仕様の導出

    廣田樹、結縁祥冶、東道徹也

    信学技報   114 巻 ( 271 ) 頁： 35-40   2014年10月

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  28. 部分観測におけるMaxSATソルバを用いたスーパバイザ合成手法

    廣田樹、結縁祥冶、東道徹也

    信学技報   114 巻 ( 416 ) 頁： 79-84   2015年1月

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  29. Modelling of Bonding with Process and Events 査読有り

    Iain Phillips, Irek Ulidowski, Shoji Yuen

    Lecture Notes in Computer Science   7948 巻   頁： 141-154   2013年7月

    　詳細を見る

    記述言語：英語  

  30. Modelling and analysis of real-time systems with mutex components 査読有り

    Guoqiang Li, Xiaojuan Cai, Shoji Yuen

    International Journal of Foundations of Computer Science   25 巻 ( 4 ) 頁： 831-851   2012年6月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1142/S0129054112400382

  31. A Reversible Process Calculus and the Modelling of the ERK signalling pathway 査読有り

    Iain Phillips, Irek Ulidowski and Shoji Yuen

    In Proceedings of the 4th workshop on reversible computation RC2012     頁： 227-239   2012年7月

    　詳細を見る

    記述言語：英語  

  32. A session type systems with subject reduction 査読有り

    Keigo Imai, Shoji Yuen, and Kiyoshi Agusa

    IEICE Transaction, Infromatoin adn systems   E95-D 巻 ( 8 ) 頁： 2053--2064   2012年8月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

  33. タスクマイグレーション機能を持つマルチコアスケジューリング解析

    中堂園貴幸,結縁祥治

    信学技法   112 巻 ( 458 ) 頁： 103-108   2013年3月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

  34. 名前渡しプロセス計算における優先度ガード 査読有り

    結縁祥治, 太田正悟

    プログラミングおよびプログラミング言語ワークショップ     頁： 246-257   2011年3月

    　詳細を見る

    担当区分：筆頭著者   記述言語：日本語  

  35. Modeling and Analysis of Real -Time Systems with Mutex Components 査読有り

    Guoqiang Li, Xiaojuan Cai, Shoji Yuen

    Advances in Parallel and Distributed Computing Models   ( 3 ) 頁： 1-8   2010年4月

    　詳細を見る

    記述言語：英語  

  36. Session Type Inference in Haskell 査読有り

    Keigo Imai, Shoji Yuen, Kiyoshi Agusa

    PLACES '10: Programming Language Approaches to Concurrency and Communication-cEntric Software     頁： 43-52   2010年3月

    　詳細を見る

    記述言語：英語  

  37. コレオグラフィに基づく高信頼通信指向GUIプログラミング

    下村翔 結縁祥治

    電子情報通信学会技術研究報告(ソフトウェアサイエンス)   109 巻 ( 456 ) 頁： 127-132   2010年3月

    　詳細を見る

    記述言語：日本語  

  38. 計算資源へのアクセス能力に基づく競合検査とデッドロック検査のための型解析

    坂野吉隆 結縁祥治

    電子情報通信学会技術研究報告(ソフトウェアサイエンス)   109 巻 ( 456 ) 頁： 133-138   2010年3月

    　詳細を見る

    記述言語：日本語  

  39. Environmental Simulation of Real -Time Systems with Nested Interrupts 査読有り

    Guoqiang Li, Shoji Yuen, Masakazu Adachi

    Theoretical Aspect of Software Engineering, TASE2009     頁： 21-28   2009年7月

    　詳細を見る

    記述言語：英語  

    Interrupts are important aspects of real-time embedded
    systems to handle events in time. When there exist nested
    interrupts in a real-time system, and an urgent interrupt is
    allowed to preempt the current interrupt handling, the design
    and analysis of the system become difficult due to the lack
    of appropriate behavioral models. This paper proposes a
    compositional model for nested interrupts and an analysis
    named environmental simulation. We present a new kind of
    timed transition system, named controller automata, to treat
    interrupts. Together with an interrupt environment modeled
    as a timed automaton, and a scheduler as a timed automaton
    with semaphores, the system behaviors with nested interrupts
    are realized by a sequence of transitions with time. Although
    various verification problems for this model are undecidable
    in general, it is shown that the reachability of error states
    is practically solvable with our implementation of the environmental
    simulation by Maude.

  40. Maude による否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築

    伴潤,今井敬吾,結縁祥治

    電子情報通信学会技術研究報告(ソフトウェアサイエンス)   109 巻 ( 40 ) 頁： 49-54   2009年5月

    　詳細を見る

    記述言語：日本語  

  41. Apache Cocoon Flowscriptのモデル検査によるWeb応用プログラムの動作検証

    馬場　敬・結縁祥治・阿草清滋

    信学技報SS-0903     頁： 19-24   2009年3月

    　詳細を見る

    担当区分：筆頭著者   記述言語：日本語  

  42. 動的電圧制御システムにおける評価戦略選択に基づく高効率消費エネルギー関数型プログラミング 査読有り

    横山哲郎 今井敬吾 曾剛 冨山宏之 高田広章 結縁祥治

    情報処理学会論文誌(プログラミング)   PRO41 巻 ( 2 ) 頁： 54-69   2009年3月

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  43. Environmental simulation of real-time systems with nested interrupts in Maude 査読有り

    Li Guoqiang, Shoji Yuen, and Masakazu Adachi

        頁： 133-147   2009年3月

    　詳細を見る

    記述言語：英語  

  44. A full implementation of session types in Haskell 査読有り

    Keigo Imai, Shoji Yuen, and Kiyoshi Agusa

        頁： 44-56   2009年3月

    　詳細を見る

    記述言語：英語  

  45. *Generating priority rewrite systems for OSOS process languages 査読有り

    Irek Ulidowski and Shoji Yuen

    Information and Computation   207 巻 ( 2 ) 頁： 120-145   2009年2月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

  46. *充足可能性判定に基づくリアルタイムシステムのスケジューリング解析 査読有り

    足立正和、末次亮、結縁祥治、手嶋茂晴、佐野範佳

    組込みシステムシンポジウム2008論文集     頁： 41-49   2008年10月

    　詳細を見る

    記述言語：日本語  

  47. 通信指向プログラミングによる高信頼ソフトウェア設計

    結縁祥治

    第六回ディペンダブルシステムワークショップDSW2008論文集     頁： 135   2008年7月

    　詳細を見る

    担当区分：筆頭著者   記述言語：日本語  

  48. 通信プロセス計算とその時間拡張 招待有り 査読有り

    結縁祥治

    システム制御学会論文誌   52 巻 ( 9 ) 頁： 322-327   2008年9月

    　詳細を見る

    担当区分：筆頭著者   記述言語：日本語  

  49. Communication centered programming of integrated services with priority in home appliance network 査読有り

    Sakura Bhandari, Shoji Yuen, Kiyoshi Agusa

    In Proceedings of APSEC2007 Workshop on Service Oriented Architecture     頁： 8-15   2007年12月

    　詳細を見る

    記述言語：英語  

    We propose an extended framework of communication
    centered programming for home appliance network where
    the distributed environment is designed in the service oriented
    architecture. Home appliances are now getting connected
    to network. By exchanging messages over network,
    various appliances constitute "integrated services"
    in that the operations by the appliances are performed
    as programmed. Following the communication centered
    programming, a global description is directly given
    for interactions that involve many appliances. A behaviorally
    equivalent local description distributed for the appliances
    is derived by the end-point projection(EPP). This
    significantly eases the distributed system programming. The
    communication centered programming is originally proposed
    by Carbone et.al. Services are available at the same
    time and a certain service may or must have the precedence
    over the other services to be consistent. To cope with this,
    we introduce "priority" in the communication centered programming.
    We present a design extension for priority both
    in global descriptions and local descriptions by examples.
    We argue the end-point projection with priority towards the
    automatic derivation of local descriptions from global descriptions.

  50. A synchronization flow analysis of concurrent objects in AIBO OPEN-R programs based on communicating processes 査読有り

    Ryo Suetsugu, Shoji Yuen, Kiyoshi Agusa

    In Proceedings of 14th Asia-pacific software engineering conference APSEC2007, IEEE computer society     頁： 366-373   2007年12月

    　詳細を見る

    記述言語：英語  

    We propose a compositional analysis method for synchronization
    flow in AIBO OPEN-R programs based on
    communicating processes. Concurrent objects of AIBO programs
    with the OPEN-R API are synchronized by two types
    of signals: ready and notify. Focusing on these signals,
    we describe abstract behavior of AIBO programs in the pi-
    calculus preserving the source code structure. We modelcheck
    deadlock freeness and interactions order of AIBO
    programs based on this abstract behavior. Since a primary
    issue in model-checking is the state space explosion in the
    behavioral model, we present a decomposing method to reduce
    the combination of states of concurrent objects. Since
    our translation to the pi-calculus preserves the syntactical
    structure of source code, when a counter-example is pointed
    out, our method enables not only to detect the violation of
    property of the whole system, but also to point out which
    component may cause the violation. We developed a prototype
    translator from AIBO OPEN-R programs to abstract
    description in the pi-calculus. We show that an application
    of our decomposing method enables to practically modelcheck
    properties by existing tools in two examples of AIBO
    programs.

  51. 通信プロセスモデルによるAIBO OPEN-Rプログラムのデッドロックフリー解析手法 査読有り

    末次亮、結縁祥治、阿草清滋

    情報処理学会論文誌   48 巻 ( 9 ) 頁： 2915-2924   2007年9月

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

    本論文ではAIBOプログラムの振る舞いを通信プロセスモデルに基づいて表現し、デッドロックフリー解析を行う手法を提案する。AIBOプログラムの標準的開発環境OPEN-Rで開発された並行オブジェクトのやりとりする同期信号に基づいて制御の流れを定式化し、実行においてデッドロックのないことを示す。

  52. 分散環境における家電機器の連携動作の記述手法

    バンダリさくら、結縁祥治、阿草清滋

    第５回ディペンダブルシステムワークショップ論文集     頁： 35-44   2007年7月

    　詳細を見る

    記述言語：日本語  

  53. セッション型に基づく高信頼性ネットワークプログラムのHaskell言語による実装

    今井敬吾、結縁祥治、阿草清滋

    第５回ディペンダブルシステムワークショップ論文集     頁： 95-106   2007年7月

    　詳細を見る

    記述言語：日本語  

  54. π計算におけるセッションの構造化

    今井敬吾、結縁祥治、阿草清滋

    第９回プログラミングおよびプログラミング言語ワークショップ論文集     頁： 140-154   2007年3月

    　詳細を見る

    記述言語：日本語  

  55. Haskellのための非同期局所化π計算に基づくネットワークプログラミングフレームワーク 査読有り

    今井敬吾、結縁祥治、阿草清滋

    情報処理学会論文誌(トランザクション)プログラミング   ( 47 ) 頁： 10,18   2006年10月

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  56. π計算に対する時間拡張と合同的性質 査読有り

    桑原 寛明, 結縁 祥治, 阿草 清滋

    電子情報通信学会論文誌   J89-D 巻 ( 4 ) 頁： 632,641   2006年4月

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  57. 通信プロセスモデルと形式意味論に基づくソフトウェアのモデル化 査読有り

    コンピュータソフトウェア   22 巻   頁： 22-43   2005年

    　詳細を見る

    担当区分：筆頭著者   記述言語：日本語  

  58. Towards Assurign Quality Attributes of Client Dynamic Web Applications: Identifying and Addressing the Challenges 査読有り

    Mohammed Sharaf Aun, Shoji Yuen, Kiyoshi Agusa

    Journal of Web Engineering   4 巻   頁： 144-164   2005年

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

  59. *Web Automata: A Behavioral Model of Web Applications based on the MVC 査読有り

    Shoji Yuen, Keishi Kato, Daiju Kato, Kiyoshi Agusa

    Computer Software   22 巻   頁： 44-57   2005年

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

    We propose a behavioral model of web applications
    based on the MVC(Model View and Control)
    model architecture. The MVC model architecture
    separates design concerns to improve the overall
    software quality. Since the architecture defines the
    abstract outline of the configurations, there is a
    broad gap between coding web applications and its
    behavioral property.
    We propose a behavioral model, called 'Web Automata',
    to implement the MVC architecture. We
    model the behavior of a web application with dynamic
    contents as an extension of links-automata
    proposed by Stotts et.al. As extended in the model
    checking techniques, we view a web application as a
    data-independent system, where variables appearing
    in link parameters and form inputs are attached
    to each page.
    We propose a testing framework for web applications
    based on the behavioral model. We show it
    provides testing criteria for web applications when
    we focus on the loops on the behavior automata.
    We apply our framework to the Jakarta Struts by
    presenting the extended configuration schema of
    Struts in order to describe the web automata directly.

  60. Name-passing style GUI Programming in a pi-calculus-based language Nepi 査読有り

    Atsushi Mizuno, Ken Mano, Yoshinobu Kawabe, Hiroaki Kuwabara, Shoji Yuen, Kiyoshi Agusa

    Electric Notes of Theoretical Computer Science   139 巻   頁： 145-168   2005年

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

    This paper describes name-passing style Graphic User Interface (GUI) programming in the programming language Nepi whose operational semantics is based on the rendezvous-style name-passing communication of the π-calculus. Nepi is able to have timed behavior by combining the wait prefix with the external choice. We model GUI programs by using channel-based behavioral characterization. We propose a pair of extended syntax elements `?g' and `!g' in Nepi to generate and terminate graphic components. The graphic components are accompanied by event handling processes that convert an event to specified name-passing. In the extended Nepi, a GUI program is described as the composition of graphic components, event handling processes, and function processes that implement the real function. We present an implementation of a GUI extension for Nepi programming language on Allegro Common Lisp to illustrate the features of name-passing style GUI programming in Nepi with examples. Finally, we discuss a formal treatment and verification technique based on the extended reduction semantics of Nepi.

  61. 通信プロセスモデルに基づく並行オブジェクト指向言語によるAIBOプログラムの動作記述 査読有り

    末次亮、結縁祥治、阿草清滋

    ソフトウェア工学の基礎ワークショップFOSE2005     頁： 267-276   2005年11月

    　詳細を見る

    記述言語：日本語  

  62. *Process languages with discrete relative time based on the Ordered SOS format and rooted eager bisimulation 査読有り

    Irek Ulidowski, Shoji Yuen

    The Journal of Logic and Algebraic Programming   60-61 巻   頁： 401-460   2004年12月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    We propose a uniform framework, based on the Ordered Structural Operational Semantics (OSOS)
    approach of Ulidowski and Phillips [Information and Computation 178 (1) (2002) 180], for process
    languages with discrete relative time. Our framework allows the user to select favourite process
    operators, whether they are standard operators or new application-specific operators, provided that
    they are OSOS definable and their OSOS rules satisfy several simple conditions. The obtained timed
    process languages preserve a timed version of rooted eager bisimulation preorder and the time determinacy
    property. We also propose several additional conditions on the type of OSOS definitions for
    the operators so that several other properties which reflect the nature of time passage, such as the
    maximal progress, patience and time persistence properties, are also satisfied.

  63. Name-passing style GUI programming in the π-calculus-based language Nepi 査読有り

    ARTS2004(6th AMAST Workshop on Real-Time Systems)Technical Report University of Leicester   ( 2004/28 ) 頁： 49-66   2004年

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語  

  64. FCDG に基づいたコーディングパターン 査読有り

    コンピュータソフトウェア   21 巻 ( 4 ) 頁： 27-36   2004年

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  65. 時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述 査読有り

    桑原寛明、結縁祥治、阿草清滋

    情報処理学会論文誌   45 巻 ( 6 ) 頁： 1498-1507   2004年

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

    組み込みシステムなどのプログラミングに用いられるオブジェクト指向言語の時間特性を形式的に記述することによってその振る舞いをできるだけ精密に特徴づけた。π計算に時間経過を導入するによって、オブジェクトの時間的振る舞いを定式化する。このことによって、小規模な実時間システムのプログラムの検証の直接的な基盤モデルを確立した。

  66. An Approach for Debugging Client Dynamic Web Applications 査読有り

    Mohammed Sharaf Aun, Shoji Yuen, Kiyoshi Agusa

      45 巻   頁： 2373-2383   2004年

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

  67. π計算に対する時間拡張と代数的意味論 査読有り

    桑原寛明、結縁祥治、阿草清滋

    ソフトウェア工学の基礎ワークショップFOSE2004     頁： 97-108   2004年11月

    　詳細を見る

    記述言語：日本語  

  68. 時間オートマトンの遷移制約記述に基づくAIBOプログラムスケルトンコードの生成手法 査読有り

    末次亮、結縁祥治、阿草清滋

    組込みソフトウェアシンポジウム2004     頁： 126-133   2004年10月

    　詳細を見る

    記述言語：日本語  

  69. Testing Framework for Web Applications based on the MVC model with Behavioral Description 査読有り

    Shoji Yuen, Keishi Kato, Daiju Kato, Shinichiro Yamamoto, Kiyoshi Agusa

    Proceedings of ICITA     頁： 11-4:1-6   2004年1月

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語  

  70. 実行可能なメモリモデルに基づくJava並行プログラムのモデル検査 査読有り

    深谷直彦、結縁祥治、阿草清滋

    ソフトウェア工学の基礎ワークショップFOSE2003     頁： 227-238   2003年11月

    　詳細を見る

    記述言語：日本語  

  71. 時間つきπ計算によるリアルタイムオブジェクト指向言語の形式的記述 査読有り

    桑原寛明、結縁祥治、阿草清滋

    オブジェクト指向最前線     頁： 69-76   2003年8月

    　詳細を見る

    記述言語：日本語  

  72. Process Languages for Rooted Weak Preorders

    Irek Ulidowski, Shoji Yuen

    Technical Report , University of Leicester   2002 巻 ( 11 )   2002年

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（大学，研究機関等紀要）  

  73. NATによる準マルチホーム化技法 査読有り

    梶田将司、結縁祥治

    情報処理学会論文誌   42 巻 ( 12 )   2001年

    　詳細を見る

    記述言語：日本語   掲載種別：研究論文（学術雑誌）  

    本論文では、ネットワークの基幹に属さない任意の規模のネットワークが局所的なポリシーに基づいて複数のインターネット接続を行う方法を提案する。本手法では、NAT(ネットワークアドレス変換)を用いて複数の外部ネットワークをプライベートネットワークにマッピングすることによる複数接続を実現する。本技法によるマルチホーム化は、ネットワークが異なる複数のグローバルアドレスを用い、接続する側の利用者が通信先に応じて経路を選択することで、一方的に信頼性、効率の向上をもk的とするため、通常のマルチホーム化と区別し、準マルチホーム化と呼ぶ。準マルチホーム化によって、複数の対外接続を局所的なポリシーに基づいて制御することができるようになるため、実際の運営形態に応じた柔軟な負荷の分散と接続の確保が可能になる。最後に名古屋大学情報メディア教育センターにおける本技法の実現方法および評価を示す。

  74. Timed Properties for Process Languages with Time 査読有り

    Irek Ulidowski and Shoji Yuen

    In Proceedings of SCI2001, Volume XIV     頁： 344-349   2001年

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語  

    We present a uniform framework for defining timed process languages
    based on the OSOS(Ordered Structural Operational Semantics)
    approach
    proposed by Ulidowski and Phillips. Our aim is
    to develop a general method for extending arbitrary process
    languages with temporal actions. An application of this
    method to a process language, for example CCS or CSP,
    produces an extension of the language with additional process
    operators and the notion of time that are most suitable
    a task in hand. We review several important properties of
    time passage, for example time determinacy,
    and propose several syntactic conditions which
    guarantee these properties in a process language
    with time.

  75. General Process Languages with Time

    Irek Ulidowski, Shoji Yuen

    Technical Report, University of Leicester   2000 巻 ( 41 )   2000年

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（大学，研究機関等紀要）  

  76. Process Languages for Rooted Eager Bisimulation 査読有り

    Lecture Notes in Computer Science   1877 巻   頁： 275,289   2000年8月

    　詳細を見る

    記述言語：英語  

  77. *Testing Theory for Probabilistic Processes 査読有り

    Rance Cleaveland, Zeynep Dayar, Scott Smolka, Shoji Yuen

    Information and Computation   154 巻   頁： 93-148   1999年

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

  78. 正則な実時間通信プロセスに対するテスト擬順序の記号的特性化

    電子情報通信学会論文誌   J80-D-1 巻 ( 6 ) 頁： 474-485   1997年

    　詳細を見る

    担当区分：筆頭著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）  

  79. Extending Process Language with Time 査読有り

    Lecture Notes In Computer Science   1349 巻   1997年

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語  

  80. Fully Abstract Characterizations of Testing Preorders for Probabilistic Processes 査読有り

    Lecture Notes in Computer Science   836 巻   頁： 497-512   1994年

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語  

  81. An extension of the testing method for processes passing infinite values 査読有り

    Shoji Yuen, Toshiki Sakabe, Yasuyoshi Inagaki

    Workshop in Computing     頁： 155-173   1993年

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

  82. An Extension of the Testing Method for Processes Passing Infinite Values 査読有り

    The John Hopkins University     頁： 10:1-20   1992年8月

    　詳細を見る

    担当区分：筆頭著者   記述言語：英語  

  83. CCSによるモニタ記述の形式的記述 査読有り

    結縁祥治、坂部俊樹、稲垣康義

    電子情報通信学会論文誌   J73-D-1 巻   頁： 683-692   1990年

    　詳細を見る

    担当区分：筆頭著者   記述言語：日本語   掲載種別：研究論文（学術雑誌）  

▼全件表示

論文の先頭へ▲

書籍等出版物 2

  1. 理論計算機科学事典 査読有り

    結縁祥治（ 担当： 分担執筆 ,  範囲: 6.4 並行計算）

    朝倉書店  2022年1月 

    　詳細を見る

    総ページ数：807   担当ページ：586-603   記述言語：中国語 著書種別：事典・辞書

  2. 並行プロセスの操作的および代数的意味論

    稲垣康義、結縁祥治（ 担当： 共著）

    丸善  1993年 

    　詳細を見る

    記述言語：日本語

書籍等出版物の先頭へ▲

講演・口頭発表等 9

  1. Nested Timed Automataに対するZoneに基づく到達可能性解析

    城聖一郎,小川瑞史,結縁祥治

    電子情報通信学会ソフトウェアサイエンス研究会  2024年3月7日  電子情報通信学会

    　詳細を見る

    開催年月日： 2024年3月

    記述言語：日本語   会議種別：口頭発表（一般）  

    開催地：石垣市健康福祉センター   国名：日本国  

  2. Bidirectional Flow analysis for a concurrent reversible programming language

    Shoji Yuen

    2024年2月28日 

    　詳細を見る

    開催年月日： 2024年2月

    記述言語：英語   会議種別：公開講演，セミナー，チュートリアル，講習，講義等  

    開催地：University of Urbino, Italy   国名：イタリア共和国  

    We present bidirectional data flow analysis for constant propagation
    in the concurrent reversible intermediate language, CRIL, proposed by
    the authors. A CRIL program is a collection of basic blocks. Each
    basic block consists of one 3-address code with labels for forward and
    backward control flow. CRIL extends RIL, proposed by Mogensen,
    allowing the multiple calls of basic blocks to execute concurrently in
    forward and backward directions. The operational semantics enjoy
    causal safety and causal liveness as the fundamental correctness for
    reversibility.

    We present a bidirectional flow analysis for CRIL programs by
    constructing a control flow graph for a CRIL program with possible
    data flow between threads via shared variables. It is shown that the
    forward and backward data flow edges cover all the data flows in
    executing the program in either direction. Based on the flow
    analysis, we further propose a syntactic translation to SSA forms with
    reversibility for optimizing CRIL programs. We propose the method for
    constant propagation and common sub-expression elimination.

    その他リンク： https://www.uniurb.it/novita-ed-eventi/5685

  3. Constant Propagation in CRIL by Bidirectional Data Flow Analysis

    Shunya Oguchi and Shoji Yuen

    2024年1月11日 

    　詳細を見る

    開催年月日： 2024年1月

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：日本国  

    We present bidirectional data flow analysis for constant propagation in the concurrent reversible intermediate
    language, CRIL, proposed by the authors. A CRIL program consists of basic blocks, each with one instruction
    enclosed by entry and exit labels. In CRIL, basic blocks are executed concurrently in forward and backward directions,
    keeping causal safety and causal liveness as the fundamental correctness for reversibility. To optimize CRIL programs,
    we focus on bidirectional data flow among basic blocks. We propose data flow analysis among basic blocks to reveal
    data flow conflicts in both directions. The bidirectional data flow analysis enables the backward constant propagation
    in addition to the forward one. We define directed edges labeled variables among basic blocks for possible forward
    data flows and give directed edges for possible backward data flows using the edges of foward data flows. It is shown
    that the forward and backward data flow edges cover all the data flows in executing the program in either direction.
    Based on this soundness property, if a constant propagates by the data flow edges, then it propagates in all concurrent
    executions of both directions. We show bidirectional constant propagation in a CRIL example by the data flow
    analysis.

  4. 充足可能性判定を利用した実現可能な時間オートマトンの検証

    城　聖一郎,結縁祥治

    電子情報通信学会ソフトウェアサイエンス研究会  2022年7月29日  電子情報通信学会

    　詳細を見る

    開催年月日： 2022年7月

    記述言語：日本語   会議種別：口頭発表（一般）  

    開催地：札幌市   国名：日本国  

  5. 通信プロセスに対する文脈変換手法を用いたモデル検査

    木川泰夫、結縁祥治、坂部俊樹

    電子情報通信学会コンピュテーション研究会 

    　詳細を見る

    開催年月日： 1999年

    記述言語：日本語   会議種別：口頭発表（一般）  

    国名：日本国  

    電子情報通信学会技術報告COMP98-82, pp.25-32

  6. 時間オートマトンによる振舞いモデルに基づく高信頼Real-time Javaコード生成手法

    井上公博、結縁祥治、阿草清滋

    電子情報通信学会ソフトウェアサイエンス研究会 

    　詳細を見る

    開催年月日： 2005年3月

    記述言語：日本語   会議種別：口頭発表（一般）  

    国名：日本国  

  7. Communication Centered Programming of Integrated Services with Priority in Home Appliance Network 国際会議

    BASICS 2009 International Workshop on Computation and Interaction, Shianghai Jiao Tong University 

    　詳細を見る

    開催年月日： 2009年10月

    記述言語：英語   会議種別：口頭発表（一般）  

    We propose an extended framework of communication centered programming for home appliance network where the distributed environment is designed in the service oriented architecture. Home appliances are now getting connected to network. By exchanging messages over network, various appliances constitute "integrated services" in that the operations by the appliances are performed as programmed. Following the communication centered programming, a global description is directly given for interactio

  8. Session types in OCaml 国際会議

    Keigo Imai, Nobuko Yoshida, Shoji Yuen

    Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051) 

    　詳細を見る

    開催年月日： 2017年1月 - 2017年2月

    記述言語：英語   会議種別：口頭発表（一般）  

    国名：ドイツ連邦共和国  

  9. タスクマイグレーション機能を持つマルチコアスケジューリング解析

    中堂園貴幸, 結縁祥治

    電子情報通信学会ソフトウェアサイエンス研究会 

    　詳細を見る

    開催年月日： 2013年3月

    記述言語：日本語   会議種別：口頭発表（一般）  

    国名：日本国  

▼全件表示

講演・口頭発表等の先頭へ▲

共同研究・競争的資金等の研究課題 4

  1. 実用上効率的な振舞いに基づくソフトウェア検証の数理的構造

    2015年3月 - 2017年12月

    二国間交流事業共同研究 

    　 詳細を見る

    資金種別：競争的資金

  2. 高信頼車載システムの検証手法の研究

    2007年4月 - 2009年3月

    国内共同研究 

    　 詳細を見る

    車載ソフトウェアの不具合を開発段階で発見することをねらいとして，形式手法を取り入れた設計方法論と検証手法を開発する。具体的には，組込みソフトウェアにおける外部からの割込みの影響を含めて，タスクスケジューラビリティを解析する手法を開発する．

  3. Webアプリケーション指向ソフトウェアモデリング

    2002年11月 - 2006年3月

    科学技術振興機構　さきがけ研究 

    　 詳細を見る

    資金種別：競争的資金

    Webアプリケーションの意味論の基礎を成す形式体系、さらに、これらに基づいて提案されている言語、形式モデルとは独立に提案されている言語などを検討し、新たな計算モデルの形式化を行う。

  4. 構造的操作意味定義に基づく実時間並行ソフトウェアの振舞い解析に関する研究

    2001年 - 2002年

    日本学術振興会 

    　 詳細を見る

    資金種別：競争的資金

共同研究・競争的資金等の研究課題の先頭へ▲

科研費 2

  1. コレオグラフィ記述に基づく組込みシステムの高信頼性設計技法

    2007年

    科学研究費補助金  基盤研究（Ｃ）（一般），課題番号：19500026

    結縁　祥治

    　 詳細を見る

    担当区分：研究代表者 

  2. データと時間を扱うオートマトンネットワークの合成的アクティブ学習に基づく設計手法

    研究課題/研究課題番号：21H03415  2021年4月 - 2026年3月

    日本学術振興会  基盤研究(B)

    　 詳細を見る

    担当区分：研究代表者  資金種別：競争的資金

    配分額：17030000円 （ 直接経費：13100000円 、 間接経費：3930000円 ）

科研費の先頭へ▲

産業財産権 1

  1. ウィジェット操作方法、装置、プログラムおよびこのプログラムを記録した記録媒体

    真野健、河辺義信、水野敦、桑原寛明、結縁祥治、阿草清滋

    　詳細を見る

    出願人：日本電信電話株式会社

    出願番号：特願2004-165578  出願日：2004年6月

    出願国：国内  

産業財産権の先頭へ▲
 

担当経験のある科目 (本学) 4

  1. 基礎セミナーＡ

    2011

  2. 知的インタフェース学特論

    2001

  3. 計算機リテラシおよびプログラミング

    2001

  4. 計算機基礎数理

    2000

担当経験のある科目 (本学)の先頭へ▲

担当経験のある科目 (本学以外) 1

  1. 情報工学概論

    2006年4月 - 2007年3月 （名城大学）

担当経験のある科目 (本学以外)の先頭へ▲