2022/12/08 更新

写真a

ウエダ カズノリ
上田 和紀
Scopus 論文情報  
論文数: 0  Citation: 0  h-index: 3

Citation Countは当該年に発表した論文の被引用数

所属
理工学術院 基幹理工学部
職名
教授

他学部・他研究科等兼任情報

  • 理工学術院   大学院基幹理工学研究科

学内研究所・附属機関兼任歴

  • 2020年
    -
    2022年

    理工学術院総合研究所   兼任研究員

学歴

  •  
    -
    1983年

    東京大学   工学系研究科   情報工学専門課程  

  •  
    -
    1978年

    東京大学   工学部   計数工学科  

学位

  • 1986年   東京大学   工学博士

  • Doctor of Engineering

経歴

  • 2010年
    -
    継続中

    エジプト日本科学技術大学客員教授

  • 2007年
    -
    継続中

    早稲田大学理工学術院情報理工学科教授

  • 2006年
    -
    2016年

    国立情報学研究所客員教授

  • 2011年
    -
    2012年

    東京大学理学部 非常勤講師

  • 2003年
    -
    2007年

    早稲田大学理工学部コンピュータ・ネットワーク工学科 教授

  • 1997年
    -
    2003年

    早稲田大学理工学部情報学科 教授

  • 2000年
    -
    2001年

    シンガポール国立大学計算機科学科 客員研究員

  • 1994年
    -
    2000年

    東京大学理学部 非常勤講師

  • 1993年
    -
    1997年

    早稲田大学理工学部情報学科 助教授

  • 1994年
    -
    1995年

    茨城大学工学部 非常勤講師

  • 1983年
    -
    1993年

    日本電気株式会社C&Cシステム研究所

  • 1985年
    -
    1992年

    日本電気株式会社より財団法人新世代コンピュータ技術開発機構に出向

▼全件表示

所属学協会

  •  
     
     

    IEEE Computer Society

  •  
     
     

    Association for Computing Machinary

  •  
     
     

    人工知能学会

  •  
     
     

    情報処理学会

  •  
     
     

    日本ソフトウェア科学会

 

研究分野

  • ソフトウェア

  • 情報学基礎論

研究キーワード

  • 論理・制約プログラミング

  • ハイブリッドシステム

  • 並行並列計算

  • プログラミング言語の設計と実装

論文

  • Constraint-Based Modeling and Symbolic Simulation of Hybrid Systems with HydLa and HyLaGI.

    Yunosuke Yamada, Masashi Sato, Kazunori Ueda

    Cyber Physical Systems. Model-Based Design. CyPhy 2019, WESE 2019. Lecture Notes in Computer Science   11971   153 - 178  2020年02月  [査読有り]

    DOI

    Scopus

  • Smart SE: Smart Systems and Services Innovative Professional Education Program

    Hironori Washizaki, Kenji Tei, Kazunori Ueda, Hayato Yamana, Yoshiaki Fukazawa, Shinichi Honiden, Shoichi Okazaki, Nobukazu Yoshioka, Naoshi Uchihira

    2020 IEEE 44th Annual Computers, Software, and Applications Conference (COMPSAC)     1113 - 1114  2020年  [査読有り]

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • Declarative Semantics of the Hybrid Constraint Language HydLa.

    Kazunori Ueda, Hiroshi Hosobe, Daisuke Ishii

    CoRR   abs/1910.12272  2019年  [査読有り]

  • Introducing Symmetry to Graph Rewriting Systems with Process Abstraction

    Taichi Tomioka, Yutaro Tsunekawa, Kazunori Ueda

    Graph Transformation. ICGT 2019. Lecture Notes in Computer Science   11629   3 - 20  2019年  [査読有り]

    DOI

    Scopus

  • Generation of Efficient Obfuscated Code through Just-in-Time Compilation.

    Muhammad Hataba, Ahmed El-Mahdy, Kazunori Ueda

    IEICE Trans. Inf. Syst.   102-D ( 3 ) 645 - 649  2019年  [査読有り]

  • Logic/Constraint Programming and Concurrency: The hard-won lessons of the Fifth Generation Computer project.

    Kazunori Ueda

    Sci. Comput. Program.   164   3 - 17  2018年  [査読有り]

    担当区分:筆頭著者

    DOI

    Scopus

    3
    被引用数
    (Scopus)
  • Implementation of LMNtal Model Checkers: a Metaprogramming Approach.

    Yutaro Tsunekawa, Taichi Tomioka, Kazunori Ueda

    J. Object Technol.   17 ( 1 ) 1 - 28  2018年  [査読有り]

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • Name Binding is Easy with Hypergraphs.

    Alimujiang Yasen, Kazunori Ueda

    IEICE Trans. Inf. Syst.   101-D ( 4 ) 1126 - 1140  2018年  [査読有り]

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • Symbolic Analysis of Hybrid Systems Involving Numerous Discrete Changes Using Loop Detection.

    Kenichi Betsuno, Shota Matsumoto, Kazunori Ueda

    Cyber Physical Systems. Design, Modeling, and Evaluation. CyPhy 2016. Lecture Notes in Computer Science   10107   17 - 30  2017年01月  [査読有り]

    DOI

    Scopus

    2
    被引用数
    (Scopus)
  • Unification of Hypergraph \lambda -Terms.

    Alimujiang Yasen, Kazunori Ueda

    Topics in Theoretical Computer Science. TTCS 2017. Lecture Notes in Computer Science   10608   106 - 124  2017年  [査読有り]

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • MEC: Network Optimized Multi-stage Erasure Coding for Scalable Storage Systems.

    Hiroaki Akutsu, Takahiro Yamamoto, Kazunori Ueda, Hideo Saito

    2017 IEEE 22nd Pacific Rim International Symposium on Dependable Computing (PRDC)     292 - 300  2017年  [査読有り]

    DOI

    Scopus

  • Symbolic Simulation of Parametrized Hybrid Systems with Affine Arithmetic

    Shota Matsumoto, Kazunori Ueda

    2016 23rd International Symposium on Temporal Representation and Reasoning (TIME)     4 - 11  2016年10月  [査読有り]

    DOI

  • Implementation of LMNtal Model Checkers: a Metaprogramming Approach.

    Yutaro Tsunekawa, Taichi Tomioka, Kazunori Ueda

    First Workshop on Meta-Programming Techniques and Reflection (META'16), Amsterdam    2016年10月  [査読有り]

  • グラフ書換え系のための効率的なグラフ正規化手法

    宮原 和大, 上田 和紀

    コンピュータ ソフトウェア   33 ( 1 ) 1_126 - 1_149  2016年

     概要を見る

    グラフ書換え系をモデリング形式とするモデル検査は高い表現力と対称性吸収機能を備えているが,検査の過程で生成されるグラフ構造の管理においてグラフ同型性判定を頻繁に行う.グラフ構造の正規化は同型なグラフが同一の表現となるようなグラフの一意表現を求める手法であり,一意表現の比較によって同型性判定を行うことができるようになるため,多数のグラフ間の同型性判定に有効である.したがって,グラフ書換え系における効率的なグラフ正規化は重要な課題といえる.本論文では彩色単純グラフを対象としたMcKay のグラフ正規化アルゴリズムにおいて,グラフ書換えに伴って変化しないグラフ構造の情報を再利用する最適化手法を提案する.再利用の実現のために,McKayのアルゴリズムの実行過程で算出される情報がグラフ構造のどの部分を反映したものかを定式化し,再計算が必要となる情報とそうでないものを区別しながら新たなグラフの正規化を行う手法を構築した.提案手法による最適化の効果を実験的に評価し,多くの場合について,頂点数に対して線形オーダを下回る時間計算量で新たな正規化が行えることを確認した.

    DOI CiNii

  • グラフ書換え系のための効率的なグラフ正規化手法

    宮原 和大, 上田 和紀

    コンピュータソフトウェア   33 ( 1 ) 126 - 149  2016年01月  [査読有り]

  • Logic/Constraint Programming and Concurrency: The Hard-Won Lessons of the Fifth Generation Computer Project

    Kazunori Ueda

    Proc. 13th International Symposium on Functional and Logic Programming (FLOPS 2016)     1 - 11  2016年  [招待有り]

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • Reliability and Failure Impact Analysis of Distributed Storage Systems with Dynamic Refuging

    Hiroaki AKUTSU, Kazunori UEDA, Takeru CHIBA, Tomohiro KAWAGUCHI, Norio SHIMOZONO

    IEICE Transactions on Information and Systems   E99.D ( 9 ) 2259 - 2268  2016年  [査読有り]

    DOI

  • HyLaGI: Symbolic Implementation of a Hybrid Constraint Language HydLa

    Shota Matsumoto, Fumihiko Kono, Teruya Kobayashi, Kazunori Ueda

    Electronic Notes in Theoretical Computer Science   317   109 - 115  2015年11月  [査読有り]

    DOI

    Scopus

    3
    被引用数
    (Scopus)
  • Reliability Analysis of Highly Redundant Distributed Storage Systems with Dynamic Refuging

    Hiroaki Akutsu, Kazunori Ueda, Takeru Chiba, Tomohiro Kawaguchi, Norio Shimozono

    2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing     261 - 268  2015年03月  [査読有り]

    DOI

  • 非線形ハイブリッドシステムの可到達集合の精度保証

    石井 大輔, 上田 和紀

    計測と制御   53 ( 12 ) 1086 - 1092  2014年12月  [査読有り]

    DOI CiNii

  • Towards a Substrate Framework of Computation

    Kazunori Ueda

    Concurrent Objects and Beyond, Lecture Notes in Computer Science   8665   341 - 366  2014年  [査読有り]  [招待有り]

    担当区分:筆頭著者

    DOI

    Scopus

    2
    被引用数
    (Scopus)
  • LMNtal並列モデル検査における状態生成数削減及び高速化

    安田竜, 吉田健人, 上田和紀

    人工知能学会論文誌   29 ( 1 ) 182 - 187  2014年01月  [査読有り]

     概要を見る

    SLIM is an LMNtal runtime. LMNtal is a programming and modeling language based on hierarchical graph rewriting. SLIM features automata-based LTL model checking that is one of the methods to solve accepting cycle search problems. Parallel search algorithms OWCTY and MAP used by SLIM generate a large number of states for problems having and accepting cycles. Moreover, they have a problem that performance seriously falls for particular problems. We propose a new algorithm that combines MAP and Nested DFS to remove states for problems including accepting cycles. We experimented the algorithm and confirmed improvements both in performance and scalability.

    DOI CiNii

    Scopus

  • ハイブリッド制約言語HydLaの記号実行シミュレータHyrose 松本 翔太, 上田 和紀

    松本 翔太, 上田 和紀

    コンピュータソフトウェア   30 ( 4 ) 18 - 35  2013年11月  [査読有り]

  • ハイブリッド制約言語プログラムのハイブリッドオートマトンへの変換アルゴリズム

    竹口輝, 和田亮, 松本翔太, 細部博史, 上田和紀

    日本ソフトウェア科学会第29回大会論文集   ( 2A-3 ) 1 - 10  2012年08月

  • HydLa: A High-Level Language for Hybrid Systems (short paper)

    Kazunori Ueda, Shota Matsumoto, Akira Takeguchi, Hiroshi Hosobe, Daisuke Ishii

    Proceedings of the 2nd Workshop on Logics for System Analysis (LfSA2012) at CAV2012     3 - 17  2012年07月  [査読有り]

  • HyperLMNtal: An Extension of a Hierarchical Graph Rewriting Model

    Kazunori Ueda, Seiji Ogawa

    KI - Künstliche Intelligenz   26 ( 1 ) 27 - 36  2012年02月  [査読有り]

    DOI

    Scopus

    7
    被引用数
    (Scopus)
  • LMNtal実行時処理系の並列モデル検査器への発展

    後町 将人, 堀 泰祐, 上田 和紀

    コンピュータ ソフトウェア   28 ( 4 ) 137 - 157  2011年11月  [査読有り]

  • An Interval-Based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    International Journal on Software Tools for Technology Transfer   13 ( 5 ) 449 - 461  2011年10月  [査読有り]

  • ハイブリッドシステムモデリング言語HydLaの実装

    松本翔太, 櫻庭翔, 高田賢士郎, 細部博史, 上田和紀

    日本ソフトウェア科学会第28回大会論文集   ( 6.00E-04 ) 1 - 11  2011年09月

  • ハイブリッドシステムモデリング言語HydLa処理系における実行アルゴリズム

    渋谷俊, 高田賢士郎, 細部博史, 上田和紀

    コンピュータソフトウェア   28 ( 3 ) 167 - 172  2011年07月  [査読有り]

  • ハイブリッドシステムモデリング言語HydLaの数式処理実行系

    高田賢士郎, 渋谷俊, 細部博史, 上田和紀

    情報処理学会第73回全国大会講演論文集     247 - 248  2011年03月

  • 強連結成分の性質を用いたOWCTYモデル検査アルゴリズムの高速化

    川端 聡基, 小林 史佳, 上田 和紀

    人工知能学会論文誌   26 ( 2 ) 341 - 346  2011年  [査読有り]

     概要を見る

    Model checking is an exhaustive search method of verification. Automata-based LTL model checking is one of the methods to solve accepting cycle search problems. Model checking is prone to state-space explosion, and we may expect that parallel processing would be a promising approach. However, the optimal sequential algorithm is based on post-order depth-first seach and is difficult to parallelize. Alternative parallel algorithms have been proposed, and OWCTY_reversed is one of them. OWCTY_reversed is known to be a stable and fast algorithm for models that accept some words, but it does not use the characteristics of the automata used in LTL model checking. We propose a new algorithm named SCC-OWCTY that exploits the SCCs (strongly connected components) of property automata. The algorithm removes states that are judged not to form accepting cycles faster than OWCTY_reversed. We experimented and compared the two algorithms using DiVinE, and confirmed improvements both in performance and scalability.

    DOI CiNii

    Scopus

  • ハイブリッド制約言語HydLaの宣言的意味論

    上田和紀, 細部博史, 石井大輔

    コンピュータソフトウェア   28 ( 1 ) 306 - 311  2011年01月  [査読有り]

    担当区分:筆頭著者

    CiNii

  • 統合開発環境によるLMNtalモデル検査

    綾野 貴之, 堀 泰祐, 岩澤 宏希, 小川 誠司, 上田 和紀

    コンピュータソフトウェア   27 ( 4 ) 197 - 214  2010年11月  [査読有り]

  • ハイブリッド制約言語HydLaの宣言的意味論

    上田和紀, 細部博史, 石井大輔

    日本ソフトウェア科学会第27回大会論文集   ( 4A-3 ) 1 - 6  2010年09月

  • ハイブリッドシステムモデリング言語HydLa処理系における実行アルゴリズム

    渋谷俊, 高田賢士郎, 上田和紀, 細部博史

    日本ソフトウェア科学会第27回大会論文集   ( 1B-2 ) 1 - 6  2010年09月

  • ハイブリッドシステムモデリング言語HydLa処理系の実行アルゴリズムの検討

    渋谷俊, 高田賢士郎, 上田和紀, 細部博史

    第8回ディペンダブルシステムワークショップ(DSW2010)論文集   ( 8月2日 ) 1 - 4  2010年07月

  • ハイブリッドシステムモデリング言語HydLaの区間制約に基づく全解シミュレーション実行処理系

    大谷順司, 廣瀬賢一, 石井大輔, 細部博史, 上田和紀

    情報処理学会創立50周年記念(第72回)全国大会論文集     145 - 146  2010年03月

  • LMNtal as a Hierarchical Logic Programming Language

    UEDA K.

    Theoretical Computer Science   410 ( 46 ) 4784 - 4800  2009年11月  [査読有り]

    担当区分:筆頭著者

    DOI CiNii

    Scopus

    13
    被引用数
    (Scopus)
  • An Interval-based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Proceedings of the Workshop on Verified Software: Theory, Tools, and Experiments (VSTTE2009)   ( 4 ) 1 - 9  2009年11月  [査読有り]

  • Interval-based Solving of Hybrid Constraint Systems

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe, Alexandre Goldsztejn

    Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS2009)     144 - 149  2009年09月  [査読有り]

  • 制約階層によるハイブリッドシステムのモデリング手法

    廣瀬賢一, 大谷順司, 石井大輔, 細部博史, 上田和紀

    日本ソフトウェア科学会第26回大会論文集   ( 2D-2 ) 1 - 10  2009年09月

  • Simulation of Hybrid Systems based on Hierarchical Interval Constraints (poster)

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Proceedings of the 2nd International Conference on Simulation Tools and Techniques (SIMUTools2009)   ( 37 ) 1 - 2  2009年03月  [査読有り]

  • c-sat : A Parallel SAT Solver for Clusters

    OHMURA K.

    Proc. SAT 2009   5584   524 - 537  2009年  [査読有り]

    DOI CiNii

    Scopus

    31
    被引用数
    (Scopus)
  • Hierarchical Graph Rewriting as a Unifying Tool for Analyzing and Understanding Nondeterministic Systems

    Kazunori Ueda, Takayuki Ayano, Taisuke Hori, Hiroki Iwasawa, Seiji Ogawa

    Theoretical Aspects of Computing - ICTAC 2009, Lecture Notes in Compter Science   5684   349 - 355  2009年  [査読有り]

    DOI

    Scopus

    7
    被引用数
    (Scopus)
  • 微分制約論理式によるハイブリッドシステムのモデリングと検証

    石井大輔, 上田和紀, 細部博史

    電子情報通信学会コンカレント工学研究会(CST), 信学技報   108 ( 415 ) 67 - 70  2009年01月

  • 制約概念に基づくハイブリッドシステムモデリング言語HydLa

    上田和紀, 石井大輔, 細部博史

    第5回システム検証の科学技術シンポジウム(SSV2008)予稿集     1 - 6  2008年11月

  • ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法

    石井大輔, 上田和紀, 細部博史

    情報処理学会論文誌:数理モデル化と応用   1 ( 1 ) 149 - 159  2008年09月  [査読有り]

  • 区間演算を用いたODE Solverにおける任意精度演算の導入とパラメタ最適化

    廣瀬 賢一, 石井 大輔, 上田 和紀

    情報科学技術フォーラム講演論文集   7 ( 1 ) 75 - 78  2008年08月

  • 論理・制約プログラミングと並行計算

    上田 和紀

    コンピュータソフトウェア   25 ( 3 ) 49 - 54  2008年08月  [査読有り]

    担当区分:筆頭著者

  • ハイブリッドシステムの高信頼シミュレーションへの区間ニュートン法の適用

    石井大輔, 上田和紀, 細部博史

    第6回ディペンダブルシステムワークショップ(DSW2008)論文集     101 - 104  2008年07月

  • 階層グラフ書換え言語LMNtalの処理系

    村山 敬, 工藤 晋太郎, 櫻井 健, 水野 謙, 加藤 紀夫, 上田 和紀

    コンピュータソフトウェア   25 ( 2 ) 47 - 77  2008年05月  [査読有り]

  • Encoding Distributed Process Calculi into LMNtal

    Kazunori Ueda

    Electronic Notes in Theoretical Computer Science   209   187 - 200  2008年04月  [査読有り]

    担当区分:筆頭著者

    DOI

    Scopus

    9
    被引用数
    (Scopus)
  • ハイブリッドシステムの高信頼性シミュレーションのための区間に基づく制約伝播手法

    石井大輔, 上田和紀, 細部博史

    情報処理学会研究報告:数理モデル化と問題解決(MPS)   68   133 - 136  2008年03月

  • 数式処理・quantifier eliminationを用いたハイブリッドシステムのZeno状態の導出手法

    大野 善之, 石井 大輔, 上田 和紀

    人工知能学会全国大会論文集 1D1-3    2008年

  • 階層グラフ書換えモデルに基づく統合プログラミング言語LMNtal

    乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀

    コンピュータソフトウェア   25 ( 1 ) 124 - 150  2008年01月  [査読有り]

    CiNii

  • ハイブリッド並行制約プログラミングにおける分岐を含む軌道の区間包囲の求解手法

    石井大輔, 上田和紀, 細部博史

    日本ソフトウェア科学会第24回大会論文集   ( 6C-1 ) 1 - 6  2007年09月

  • A Branching Approach to the Interval-based Evaluation of Ask Constraints in Hybrid CCP

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Proc. CP 2007 Doctoral Programme, the 13th Int. Conf. on Principles and Practice of Constraint Programming (CP2007)     49 - 54  2007年09月

  • SATソルバMiniSatの並列化とそのチューニング手法

    大村圭, 渋谷健介, 稲垣良一, 上田和紀

    情報処理学会研究報告   2007 ( 80 ) 31 - 36  2007年08月

     概要を見る

    本論文では、充足可能性問題(SAT)の逐次ソルバである MiniSat の lemma 共有を用いた並列化とそのチューニング手法について述べる。SAT ソルバは特定の探索域には解がないということを lemma と呼ばれる clause として学習する。この lemma は探索木の枝刈りに非常に有効であるが、全ての lemma を各 PE 間で共有するためには膨大な通信コストがかかってしまうため、効率の良い学習と通信が必要である。lemma の渡し方や各パラメタをチューニングし、24PE のクラスタで実行したところ、逐次版では解けなかった問題のうち、27 題を新たに解くことができた。This paper describes parallelization of the SAT solver MiniSat based on lemma sharing and its tuning techniques. When an SAT solver finds that a specific branch of the search space does not have a solution, it learns new clauses called lemmas. Lemmas are very useful for pruning search space. However, since sharing lemmas between PEs can take enormous communication cost, developing efficient learning and communication techniques is very important. Using parameters obtained by various experiments on lemma sharing, our parallel MiniSAT solved many more SAT competition problems than the original MiniSAT on a PC cluster with 24 PEs.

    CiNii

  • モデル検査器SPINにおける状態空間の性質の調査

    渋谷健介, 上田和紀

    第5回ディペンダブルシステムワークショップ(DSW2007)論文集     9 - 12  2007年07月

  • 数式処理に基づくハイブリッドシステムにおけるZenonessの判定手法

    大野善之, 石井大輔, 上田和紀

    第5回ディペンダブルシステムワークショップ論文集     53 - 56  2007年07月

  • An Interval-based Approximation Method for Discrete Changes in Hybrid cc

    Daisuke Ishii, Kazunori Ueda, Hroshi Hosobe

    Trends in Constraint Programming     245 - 255  2007年05月  [査読有り]

  • 階層グラフ可視化ツール"UNYO-UNYO"(うにょうにょ)の設計と実装

    中野敦, 上田和紀

    第9回プログラミングおよびプログラミング言語ワークショップ (PPL2007)    2007年03月

  • 純粋λ計算の階層グラフ書換えへのエンコーディング

    上田和紀

    第9回プログラミングおよびプログラミング言語ワークショップ (PPL2007)     221 - 232  2007年03月

  • Hierarchical graph rewriting as a unifying model of concurrency

    Kazunori Ueda

    LIX Colloquium on Emerging Trends in Concurrency Theory    2006年11月  [招待有り]

  • 後継関数を持つリスト型非線形再帰プログラムに対する再帰除去法

    市川祐輔, 上田和紀

    情報科学技術レターズ   6   9 - 12  2006年09月  [査読有り]

  • 分散プロセス計算のLMNtalへのエンコーディング

    上田和紀

    日本ソフトウェア科学会第23回大会論文集     1A - 4  2006年09月

  • Hybrid cc における区間計算に基づいた離散変化処理方式

    石井大輔, 上田和紀, 細部博史

    日本ソフトウェア科学会第23回大会論文集     1A - 1  2006年09月

  • An Interval-based Approximation Method for Discrete Changes in Hybrid cc

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Third International Workshop on Interval Analysis, Constraint Propagation and Applications (IntCP'06)     38 - 51  2006年09月  [査読有り]

  • Constraint-Based Concurrency and Beyond

    Kazunori Ueda

    Electronic Notes in Theoretical Computer Science   162   327 - 331  2006年09月

  • LMNtal as a Unifying Declarative Language

    Kazunori Ueda, Norio Kato, Koji Hara, Ken Mizuno

    Third Workshop on Constraint Handling Rules (CHR 2006)     1 - 15  2006年07月  [招待有り]

  • Logic Programming and Concurrency: a Personal Perspective

    Kazunori Ueda

    The ALP NewsLetter   19 ( 2 )  2006年05月  [招待有り]

  • アセンブリプログラムの構造を利用したキャッシュヒント自動付加

    稲垣良一, 上田和紀

    先進的計算基盤システムシンポジウム (SACSIS2006)     59 - 66  2006年05月

  • 階層グラフ書き換え言語LMNtal処理系とその応用例

    乾敦行, 原耕司, 水野謙, 上田和紀

    第8回プログラミングおよびプログラミング言語ワークショップ (PPL2006)     119 - 133  2006年03月

  • 非決定的LMNtalとその検証への応用

    水野謙, 上田和紀

    第8回プログラミングおよびプログラミング言語ワークショップ (PPL2006)    2006年03月

  • OCamlによるLMNtal実行時処理系 OCaMNtalの実装

    工藤晋太郎, 乾敦行, 櫻井健, 上田和紀

    第8回プログラミングおよびプログラミング言語ワークショップ (PPL2006)    2006年03月

  • LMNtal as a unifying declarative language: Live demonstration

    Kazunori Ueda, Norio Kato, Koji Hara, Ken Mizuno

    LOGIC PROGRAMMING, PROCEEDINGS   4079   457 - 458  2006年  [査読有り]

  • LMNtalコンパイラにおける並び替えとグループ化を用いた命令列の最適化

    櫻井健, 加藤紀夫, 水野謙, 上田和紀

    第4回情報科学技術フォーラム (FIT2005)   A-014 ( 第一分冊 ) 33 - 36  2005年09月

  • JP ドメインにおける茶筌を用いた中国語ページの抽出

    魏小比, 内藤一兵衛, 上田和紀

    第4回情報科学技術フォーラム (FIT2005)   ( 第二分冊 ) 179 - 182  2005年09月

  • 数式処理システムMathematica上における再帰除去システム

    市川祐輔, 二村良彦, 上田和紀

    第4回情報科学技術フォーラム (FIT2005)   A-022 ( 第一分冊 ) 53 - 54  2005年09月

  • キャッシュヒント自動付加を用いたソフトウェア高速化

    稲垣良一, 上田和紀

    第4回情報科学技術フォーラム (FIT2005)   B-030 ( 第一分冊 ) 161 - 162  2005年09月

  • LMNtal処理系におけるグラフ構造の複製・破棄および比較機能の設計と実装

    工藤晋太郎, 上田和紀, 加藤紀夫

    情報科学技術レターズ   LA-003   9 - 12  2005年09月  [査読有り]

  • 階層グラフ書換え言語LMNtal処理系における非同期実行の実現

    水野謙, 加藤紀夫, 原耕司, 上田和紀

    日本ソフトウエア科学会第22回大会講演論文集     3A - 4  2005年09月

  • Constraint-Based Concurrency and Beyond

    Kazunori Ueda

    Proc. Workshop on Algebraic Process Calculi, The First Twenty Years     227 - 230  2005年08月  [招待有り]

  • 確率モデル遺伝的アルゴリズムEHBSAにおける戦略、パラメータの調査

    酒井大輔, 上田和紀

    人工知能学会全国大会(第19回)論文集     2F1 - 02  2005年06月

  • Itanium2プロセッサにおけるキャッシュヒント自動付加手法

    稲垣良一, 上田和紀

    先進的計算基盤シンポジウム SACSIS2005     218 - 219  2005年05月

  • 21世紀COEプロジェクト「プロダクティブICTアカデミア」

    上田和紀, 大石進一, 甲藤二郎, 中島達夫, 村岡洋一, 山名早人

    情報処理   46 ( 4 ) 410 - 416  2005年04月

  • 並列論理型言語のコンパイル技法

    上田和紀

    情報処理学会第67回全国大会特別セッション(6)    2005年03月

  • LMNtalを用いた分散処理の実現

    中島求, 加藤紀夫, 水野謙, 上田和紀

    第8回 プログラミングおよび応用のシステムに関するワークショップ (SPA2005)    2005年03月

  • 小規模制御系向けLMNtal処理系の設計と実装

    矢島伸吾, 加藤紀夫, 上田和紀

    第7回プログラミングおよびプログラミング言語ワークショップ (PPL2005)     41 - 41  2005年03月

  • 階層グラフ書き換えによるプロトコル検証

    圷弘明, 加藤紀夫, 上田和紀

    第7回プログラミングおよびプログラミング言語ワークショップ (PPL2005)     41 - 41  2005年03月

  • プログラムと対称性

    上田和紀

    夏のプログラミングシンポジウム「アッと驚くプログラミング」報告集     69 - 74  2005年01月

  • 20世紀の名著名論 − C. A. R. Hoare: Communicating Sequential Processes

    上田和紀

    情報処理   46 ( 1 ) 66 - 66  2005年01月

  • 言語モデルLMNtalの操作的意味論の設計

    加藤紀夫, 水野謙, 上田和紀

    日本ソフトウェア科学会第21回大会論文集     153 - 163  2004年09月

  • LMNtal分散処理系の設計と実装

    中島求, 加藤紀夫, 水野謙, 上田和紀

    日本ソフトウェア科学会第21回大会論文集     149 - 153  2004年09月

  • LMNtal処理系および他言語インタフェースの設計と実装

    原耕司, 水野謙, 矢島伸吾, 永田貴彦, 中島求, 加藤紀夫, 上田和紀

    情報処理学会第50回プログラミング研究会 (SWoPP2004)    2004年07月

  • SATソルバzchaffのMPIによる並列化

    大橋智昭, 稲垣良一, 上田和紀

    情報処理学会研究報告 2004-HPC99-5 (SWoPP2004)     25 - 30  2004年07月

  • 階層グラフ書換え言語における並行プロセスの型推論

    加藤紀夫, 上田和紀

    情報処理学会第50回プログラミング研究会 (SWoPP2004)    2004年07月

  • SMPクラスタにおける効率的なMPI集団通信関数の実装

    稲垣良一, 上田和紀

    先進的計算基盤システムシンポジウム SACSIS2003     171 - 172  2004年05月

  • SATソルバzchaffのMPIによる並列化

    大橋智昭, 上田和紀

    先進的計算基盤シンポジウム SACSIS2004   LNCS 3365, Springer-Verlag   147 - 148  2004年05月

  • 言語モデルLMNtal

    上田 和紀, 加藤 紀夫, Kazunori Ueda, Norio Kato, 早稲田大学コンピュータ・ネットワーク工学科:科学技術振興事業団, Dept. of Computer Science Waseda University:CREST Japan Science and Technology Corporation., Dept. of Computer Science Waseda University

    コンピュータソフトウェア = Computer software   21 ( 2 ) 126 - 142  2004年03月

     概要を見る

    階層的グラフの書換えを基本原理とするプログラミング言語モデルLMNtalについて,設計の背景および関連研究を交えながら解説する.LMNtal(elementalと発音)は,並行計算や多重集合書換えをはじめとするさまざまな計算に関する概念の統合を目指して設計した言語モデルであり,(1)計算モデルとして簡明であることと,(2)多様なプラットフォームで利用可能な実用プログラミング言語のベースとなること,の両立を目指している.処理系も稼働を始めている.本解説ではなるべく多くのプログラム例を交えながら,LMNtalの言語機能について解説するとともに,他の言語や計算モデルに見られる言語機能との関連付けを行なう.関連計算モデルに言及する部分は,並行計算および論理プログラミングに関する初歩的な知識があるとよりよく理解できるあろう.しかし,LMNtal自体の言語機能やプログラム例は予備知識なしで十分理解できるように解説したい.

    DOI CiNii

    Scopus

    1
    被引用数
    (Scopus)
  • 制約に基づくアニメーション作成環境 Grifon

    石井大輔, 中村好一, 大野太郎, 若槻聡一郎, 上田和紀

    情報処理学会第66回全国大会     1J - 2  2004年03月

  • 制約に基づくアニメーション作成環境 Grifon におけるデータ構造の階層化

    中村好一, 石井大輔, 大野太郎, 若槻総一郎, 上田和紀

    情報処理学会第66回全国大会     1J - 1  2004年03月

  • LMNtalルールコンパイラにおける内部命令の設計

    水野謙, 永田貴彦, 加藤紀夫, 上田和紀

    情報処理学会第66回全国大会     5G - 2  2004年03月

  • LMNtalにおけるルールセット不変性の検査

    圷弘明, 加藤紀夫, 上田和紀

    第6回プログラミングおよびプログラミング言語ワークショップ (PPL2004)     211 - 216  2004年03月

  • 並行言語モデルLMNtalにおけるプロセス構造の解析

    加藤紀夫, 上田和紀

    第6回プログラミングおよびプログラミング言語ワークショップ (PPL2004)     217 - 222  2004年03月

  • 言語モデルLMNtal

    上田和紀, 加藤紀夫

    コンピュータソフトウェア   21 ( 2 ) 44 - 60  2004年03月  [査読有り]

    CiNii

  • LMNtal: A language model with links and membranes

    K Ueda, N Kato

    Proc. Fifth Int. Workshop on Membrane Computing (WMC 2004), Lecture Notes in Computer Science   3365   110 - 125  2004年  [査読有り]  [招待有り]

     概要を見る

    LMNtal (pronounced "elemental") is a simple language model based on graph rewriting that uses logical variables to represent links and membranes to represent hierarchies. The two major goals of LMNtal are (i) to unify various computational models based on multiset rewriting and (ii) to serve as the basis of a truly general-purpose language covering various platforms ranging from wide-area to embedded computation. Another important contribution of the model is that it greatly facilitates programming with dynamic data structures.

  • The language model LMNtal

    K Ueda, N Kato

    Logic Programming. ICLP 2003. Lecture Notes in Computer Science   2916   517 - 518  2003年12月  [査読有り]

    担当区分:筆頭著者

  • Teaching (Constraint) Logic Programming

    Kazunori Ueda

    Panel at Nineteenth Int. Conf. on Logic Programming (ICLP'03)   http://www.cs.kuleuven.ac.be/~dtai/projects/ALP/ newsletter/nav/short.html  2003年12月  [招待有り]

  • LMNtalプロセスの振舞いの定式化

    加藤紀夫, 上田和紀

    日本ソフトウェア科学会第20回大会論文集   16-20   16 - 20  2003年09月

  • LMNtalプロトタイプ処理系の設計と実装

    矢島伸吾, 永田貴彦, 加藤紀夫, 上田和紀

    日本ソフトウェア科学会第20回大会論文集   21-25   21 - 25  2003年09月

    CiNii

  • 人工知能学会2002年度全国大会ベストプレゼンテーション賞

    網代育大, 上田和紀

    人工知能学会   (発表題目「反復深化A*探索によるもっともらしいプログラムの効率的生成」)  2003年04月

  • KLIC処理系におけるUNIXプロセス間通信を利用した例外処理の実装

    金木佑介, 加藤紀夫, 上田和紀

    第6回プログラミングおよび応用のシステムに関するワークショップ (SPA2003)   http://spa.jssst.or.jp/2003/program/  2003年03月

  • LMNtalプロトタイプ処理系の設計と実装

    日本ソフトウェア科学会第20回大会論文集   21-25  2003年

  • LMNtalプロセスの振舞いの定式化

    日本ソフトウェア科学会第20回大会論文集   16-20  2003年

  • KLIC処理系におけるUNIXプロセス間通信を利用した例外処理の実装

    第6回プログラミングおよび応用のシステムに関するワークショップ (SPA2003)、日本ソフトウェア科学会    2003年

  • Programming with Logical Links: Design of the LMNtal language

    Kazunori Ueda, Norio Kato

    Proc. 3rd Asian Workshop on Programming Languages and Systems (APLAS 2002)   pp.115-126   115 - 126  2002年11月

  • 分散言語処理系DKLIC の設計と実装

    高山啓, 松村量, 高木祐介, 加藤紀夫, 上田和紀

    日本ソフトウェア科学会第19回大会論文集     5F - 1  2002年09月

  • モード制約の漸近的一様補強による並行論理プログラムのoccurs-check解析

    加藤紀夫, 上田和紀

    日本ソフトウェア科学会第19回大会論文集     5F - 2  2002年09月

  • GHCからLMNtalへ

    上田和紀

    情報処理学会 2002年度 夏のプログラミングシンポジウム   http://www.ipsj.or.jp/prosym/sprosym/program/LMNtal-prosym.pdf  2002年09月

  • 20世紀の名著名論 − J. A. Robinson: A Machine-Oriented Logic Based on the Resolution Principle

    上田和紀

    情報処理   43 ( 7 ) 792 - 792  2002年07月

  • 反復深化A*探索によるもっともらしいプログラムの効率的な生成

    網代育大, 上田和紀

    人工知能学会全国大会(第17回)論文集   1E3-02   1E3 - 02  2002年06月

  • 反復深化A*探索によるもっともらしいプログラムの効率的な生成

    人工知能学会全国大会(第17回)論文集   1E3-02  2002年

  • Programming with Logical Links

    日本ソフトウェア科学会第19回大会論文集    2002年

  • モード制約の漸近的一様補強による並行論理プログラムのoccurs-check解析

    日本ソフトウェア科学会第19回大会論文集    2002年

  • Programming with Logical Links: Design of the LMNtal language

    Proc. 3rd Asian Workshop on Programming Languages and Systems (APLAS 2002)   pp.115-126  2002年

  • Sequentiality analysis for concurrent logic programs

    N Kato, K Ueda

    6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XI, PROCEEDINGS   Vol.11, pp.329-336   329 - 336  2002年

     概要を見る

    We present a bottom-up method of extracting those fragments of concurrent logic programs that can be executed sequentially, and we also propose a framework of optimizing compilation of concurrent logic programs that uses sequential intermediate code generated with the method. The method is directed by the inference of certain properties on sequentiality, called interfaces, of concurrent processes. We formalize them in terms of the operational semantics, which enables us to formally justify the inference laws on interfaces used in the analysis.
    The specialization of concurrent processes is critical for an optimizing compiler, for it can reduce the runtime overhead of process management and of data manipulation substantially. The inference laws on interfaces ensure the compositional generation of the sequential specialized code that enables such optimization. Moreover, a formal definition of the intermediate code will prove the correctness of some implementation-level optimization techniques, including tag elimination and update-in-place optimization, that cannot be formally proved by source-level analysis.
    Although the formalism of interfaces exploits the constraint-based communication feature of the language, our method can be applied, in principle, to the extraction of sequentiality in other fine-grained concurrent languages.

  • A Pure Meta-Interpreter for Flat GHC, A Concurrent Constraint Language

    Kazunori Ueda

    Computational Logic: Logic Programming and Beyond (Essays in Honour of Robert A. Kowalski, Part I), A.C. Kakas, F. Sadri (Eds.), Springer-Verlag   2407   138 - 161  2002年  [査読有り]  [招待有り]

  • Kima: An automated error correction system for concurrent logic programs

    Yasuhiro Ajiro, Kazunori Ueda

    Automated Software Engineering   9 ( 1 ) 67 - 94  2002年01月  [査読有り]

     概要を見る

    We have implemented Kima, an automated error correction system for concurrent logic programs. Kima corrects near-misses such as wrong variable occurrences in the absence of explicit declarations of program properties. Strong moding/typing and constraint-based analysis are turning out to play fundamental roles in debugging concurrent logic programs as well as in establishing the consistency of communication protocols and data types. Mode/type analysis of Moded Flat GHC is a constraint satisfaction problem with many simple mode/type constraints, and can be solved efficiently. We proposed a simple and efficient technique which, given a non-well-moded/typed program, diagnoses the "reasons" of inconsistency by finding minimal inconsistent subsets of mode/type constraints. Since each constraint keeps track of the symbol occurrence in the program, a minimal subset also tells possible sources of program errors. Kima realizes automated correction by replacing symbol occurrences around the possible sources and recalculating modes and types of the rewritten programs systematically. As long as bugs are near-misses, Kima proposes a rather small number of alternatives that include an intended program. Search space is kept small because the minimal subset confines possible sources of errors in advance. This paper presents the basic algorithm and various optimization techniques implemented in Kima, and then discusses its effectiveness based on quantitative experiments.

    DOI

    Scopus

    9
    被引用数
    (Scopus)
  • Sequentiality analysis for concurrent logic programs

    N Kato, K Ueda

    6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XI, PROCEEDINGS   Vol.11, pp.329-336   329 - 336  2002年  [査読有り]

     概要を見る

    We present a bottom-up method of extracting those fragments of concurrent logic programs that can be executed sequentially, and we also propose a framework of optimizing compilation of concurrent logic programs that uses sequential intermediate code generated with the method. The method is directed by the inference of certain properties on sequentiality, called interfaces, of concurrent processes. We formalize them in terms of the operational semantics, which enables us to formally justify the inference laws on interfaces used in the analysis.
    The specialization of concurrent processes is critical for an optimizing compiler, for it can reduce the runtime overhead of process management and of data manipulation substantially. The inference laws on interfaces ensure the compositional generation of the sequential specialized code that enables such optimization. Moreover, a formal definition of the intermediate code will prove the correctness of some implementation-level optimization techniques, including tag elimination and update-in-place optimization, that cannot be formally proved by source-level analysis.
    Although the formalism of interfaces exploits the constraint-based communication feature of the language, our method can be applied, in principle, to the extraction of sequentiality in other fine-grained concurrent languages.

  • Programming with Logical Links

    上田和紀, 加藤紀夫

    日本ソフトウェア科学会第19回大会論文集     3A - 1  2002年

  • Optimizing Compilation of Concurrent Logic Programs Directed by Interface Analysis

    Proc. Second Asian Workshop on Programming Languages and Systems   pp.237-250  2001年12月

  • Optimizing Compilation of Concurrent Logic Programs Directed by Interface Analysis

    Proc. Second Asian Workshop on Programming Languages and Systems   pp.237-250  2001年12月

  • Resource-Passing Concurrent Programming

    Proc. Second Asian Workshop on Programming Languages and Systems, KAIST, Daejeon, Korea   pp.313-328  2001年12月

  • 人工知能とソフトウェア文化

    人工知能学会誌/人工知能学会   16;6  2001年11月

  • インタフェースに基づく並行論理プログラム最適化コンパイラの構成法

    情報処理学会第36回プログラミング研究会    2001年10月

  • Resource-Passing Concurrent Programming

    Proc. Fourth Int. Symp. on Theoretical Aspects of Computer Software, Kobayashi, N. and Pierce, B. (Eds.), Springer-Verlag   LNCS 2215, pp.95-126  2001年10月  [査読有り]  [招待有り]

  • 日本ソフトウェア科学会第18回大会講演論文集

    日本ソフトウェア科学会    2001年09月

  • 計算連続体に基づくソフトウェア実現法の提案

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001年09月  [査読有り]

  • インタフェースに基づく並行論理プログラム最適化コンパイラの構成法

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001年09月

  • 制約の局所性に基づく並行論理プログラム自動修正系 Kima の最適化

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001年09月

  • 制約の局所性に基づく並行論理プログラム自動修正系 Kima の最適化

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001年09月

  • インタフェースに基づく並行論理プログラム最適化コンパイラの構成法

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001年09月

  • 計算連続体に基づくソフトウェア実現法の提案

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001年09月

  • 日本ソフトウェア科学会第18回大会講演論文集

    日本ソフトウェア科学会    2001年09月

  • MPIによるGIMP並列化

    並列処理シンポジウム (JSPP2001) 論文集,情報処理学会   pp.123-124  2001年06月

  • 日本ソフトウェア科学会第5回論文賞(論文題目“自己調整二分木の並列操作”)

    日本ソフトウェア科学会    2001年05月

  • dklic: KL1による分散KL1言語処理系の実装

    第4回プログラミングおよび応用のシステムに関するワークショップ (SPA2001),日本ソフトウェア科学会    2001年03月

  • 並列KLIC処理系上での配列演算の最適化

    情報処理学会論文誌:プログラミング   42;SIG 3(PRO 10), pp.1-13  2001年03月  [査読有り]

  • 並行論理プログラムにおける逐次実行部分の抽出方法論

    第3回プログラミングおよびプログラミング言語ワークショップ (PPL2001),日本ソフトウェア科学会   pp.2-13  2001年03月

  • dklic: KL1による分散KL1言語処理系の実装

    第4回プログラミングおよび応用のシステムに関するワークショップ (SPA2001),日本ソフトウェア科学会    2001年03月

  • 並列KLIC処理系上での配列演算の最適化

    情報処理学会論文誌:プログラミング   42;SIG 3(PRO 10), pp.1-13  2001年03月

  • TECO

    bit/共立出版   33;2, pp.48-54  2001年02月

  • Resource-Passing Concurrent Programming

    Proc. Second Asian Workshop on Programming Languages and Systems   pp.313-328  2001年

  • A Close Look at Constraint-Based Concurrency

    Proc. 17th Int. Conf. on Logic Programming, Philippe Codognet (ed.), Springer-Verlag   LNCS 2237, p.9  2001年  [招待有り]

  • Functional and Logic Programming-5th International Symposium on Functional and Logic Programming (FLOPS 2001)

    Springer-Verlag   Lecture Notes in Computer Science 2024  2001年

  • シンガポール国立大学

    人工知能学会誌   16;1, pp.169-170  2001年01月

  • Crosoeは成功するか? − 私はCrusoeを使いたい

    情報処理   41;9  2000年09月

  • Kima -- an Automated Error Correction System for Concurrent Logic Programs

    Proc. Fourth International Workshop on Automated Debugging (AADEBUG 2000)   http://www.irisa.fr/lande/ducasse/ aadebug2000/proceedings.html  2000年09月  [査読有り]

  • 並行論理プログラムのプログラム空間に関する考察

    2000年度人工知能学会全国大会(第14回)論文集   pp.449-452  2000年07月

  • Linearity Analysis of Concurrent Logic Programs

    Proc. International Workshop on Parallel and Distributed Computing for Symbolic and Irregular Applications (PDSIA'99), Ito, T. and Yuasa, T. (eds.), World Scientific   pp.253-270   253 - 270  2000年05月

  • 第五世代核言語ができるまで

    第3回システムおよびプログラミングの応用に関するワークショップ (SPA2000)    2000年03月  [招待有り]

  • 共有オブジェクト空間を用いた分散プログラミング支援ミドルウェア SOR (Shared Object Repository) とその応用例の紹介

    情報処理学会第60回全国大会講演論文集(1)   1ZB-05, pp.313-314  2000年03月

  • 並行論理プログラム自動修正系 kima における誤り検出率の向上とその効果

    情報処理学会第60回全国大会講演論文集(1)   2V-06, pp.283-284  2000年03月

  • 並行論理プログラムの静的 Occur-checker の設計と実装

    情報処理学会第60回全国大会講演論文集(1)   2V-05, pp.281-282  2000年03月

  • Java 仮想機械上で動作する分散 KL1 言語処理系の実装

    情報処理学会第60回全国大会講演論文集(1)   2H-01, pp.13-14  2000年03月

  • 存在価値のある研究会を目指して—プログラミング研究会の試み—

    情報処理学会第60回全国大会記念セッション・イベント報告集   pp.127-130  2000年03月

  • 並行論理型言語における同期ポイントの移動の安全性について

    情報処理学会論文誌:プログラミング   41 ( SIG 2(PRO 6) ) 13 - 28  2000年03月  [査読有り]

  • Kima: 並行論理プログラム自動修正系

    網代 育大, 上田 和紀

    コンピュータソフトウェア   18 ( 0 ) 122 - 137  2000年  [査読有り]

    DOI

    Scopus

    1
    被引用数
    (Scopus)
  • 共有オブジェクト空間を用いた分散プログラミング支援ミドルウェアSOR(Shared Object Repository)とその応用例の紹介

    情報処理学会第60回全国大会講演論文集(1)   /,1ZB-05,313-314  2000年

  • 並行論理プログラム自動修正系kimaにおける誤り検出率の向上とその効果

    情報処理学会第60回全国大会講演論文集(1)   /,2V-06,283-284  2000年

  • 並行論理プログラムの静的Occur-checkerの設計と実装

    情報処理学会第60回全国大会講演論文集(1)   /,2V-05,281-282  2000年

  • Java仮想機械上で動作する分散KL1言語処理系の実装

    情報処理学会第60回全国大会講演論文集(1)   /,2H-01,13-14  2000年

  • Linearity Analysis of Concurrent Logic Programs

    Proc. International Workshop on Optimization and Implementation of Declarative Programs (WOID'99), abstract also in Electronic Notes in Theoretical Computer Science 30(2)   http://www.dsse.ecs.soton.ac.uk/ techreports/  1999年11月

  • 自己調整二分木の並列操作

    コンピュータソフトウェア   16 ( 5 ) 78 - 83  1999年09月  [査読有り]

    担当区分:筆頭著者

  • 全文検索システムVernoのアーキテクチャの設計

    第2回インターネットテクノロジワークショップ (WIT'99) 論文集   pp.163-170  1999年08月

  • 分散KL1言語処理系の設計と実装

    並列処理シンポジウム(JSPP'99)論文集   p.207  1999年06月

  • KLIC並列処理系における配列演算の最適化

    並列処理シンポジウム(JSPP'99)論文集   p.208  1999年06月

  • Concurrent Logic/Constraint Programming: The Next 10 Years

    The Logic Programming Paradigm: A 25-Year Perspective, K. R. Apt, V. W. Marek, M. Truszczynski, and D. S. Warren (eds.), Springer-Verlag   pp.53-71  1999年04月  [査読有り]  [招待有り]

  • KLIC へのデータ並列処理機能の導入について

    情報処理学会第58回全国大会講演論文集/情報処理学会   4N-02  1999年03月

  • 汎用並列組合せ最適化パッケージの構想

    情報処理学会第58回全国大会講演論文集/情報処理学会   3K-02  1999年03月

  • WWW全文検索システムVernoのアーキテクチャ

    情報処理学会第58回全国大会講演論文集/情報処理学会   4T-07  1999年03月

  • オブジェクト共有空間を利用した分散プログラミング支援フレームワークSOR

    第2回プログラミングおよび応用のシステムに関するワークショップ(SPA'99)/日本ソフトウェア科学会   http://www.softlab.is.tsukuba.ac.jp/ spa99proc/  1999年03月

  • WWW全文検索システムVernoのアーキテクチャ

    情報処理学会第58回全国大会講演論文集/情報処理学会   4T-07  1999年03月  [査読有り]

  • WWW全文検索システムVernoのデータベース

    情報処理学会第58回全国大会講演論文集/情報処理学会   4T-06  1999年03月

  • 並行論理プログラムの参照数解析

    情報処理学会論文誌:プログラミング/情報処理学会   40;SIG1(PRO2),p.60  1999年02月

  • Linearity Analysis of Concurrent Logic Programs

    Electronic Notes in Theoretical Computer Science   30;2  1999年

    担当区分:筆頭著者

  • 全文検索システムVernoのアーキテクチャの設計

    第2回インターネットテクノロジワークショップ(WIT'99)論文集/日本ソフトウェア科学会   /,163-170  1999年

  • WWW全文検索システムVernoのデータベース

    情報処理学会第58回全国大会講演論文集/情報処理学会   4T-06  1999年

  • KLICへのデータ並列処理機能の導入について

    情報処理学会第58回全国大会講演論文集/情報処理学会   4N-02  1999年

  • 汎用並列組合せ最適化パッケージの構想

    情報処理学会第58回全国大会講演論文集/情報処理学会   3K-02  1999年

  • オブジェクト共有空間を利用した分散プログラミング支援フレームワークSOR

    第2回プログラミングおよび応用のシステムに関するワークショップ(SPA'99)/日本ソフトウェア科学会   http://www.softlab.is.tsukuba.ac.jp/ spa99proc/  1999年

  • ハードウェアの進歩とソフトウェアの進歩

    bit別冊「はじめての並列プログラミング」/共立出版   p.100  1998年05月

  • Bookガイド − プログラミング言語編

    bit/共立出版   30;4, pp.56-64  1998年04月

  • 分散型WWW全文収集ロボットIron33

    情報処理学会第56回全国大会論文集    1998年03月

  • 学習型WWW全文検索エンジンVerno

    情報処理学会第56回全国大会論文集    1998年03月

  • 自己調整二分木の並列操作

    上田 和紀

    日本ソフトウェア科学会第15回大会論文集     173 - 176  1998年

    担当区分:筆頭著者

  • Error-correcting source code

    Y Ajiro, K Ueda, K Cho

    Principles and Practice of Constraint Programming - CP98, Lecture Notes in Computer Science   1520   40 - 54  1998年  [査読有り]

     概要を見る

    We study how constraint-based static analysis can be applied to the automated and systematic debugging of program errors.
    Strongly moding and constraint-based mode analysis are turning to play fundamental roles in debugging concurrent logic/constraint programs as well as in establishing the consistency of communication protocols and in optimization. Mode analysis of Moded Flat GHC is a constraint satisfaction problem with many simple mode constraints, and can be solved efficiently by unification over feature graphs. We have proposed a simple and efficient technique which, given a non-well-moded program, diagnoses the "reasons" of inconsistency by finding minimal inconsistent subsets of mode constraints. Since each constraint keeps track of the symbol occurrence in the program that imposed the constraint, a minimal subset also tells possible sources of program errors. The technique is quite general and can be used with other constraint-based frameworks such as strong typing.
    Based on the above idea, we study the possibility of automated debugging an the absence of mode/type declarations. The mode constraints are usually imposed redundantly, and the constraints that are considered correct can be used for correcting wrong symbol occurrences found by the diagnosis. As long as bugs are near-misses, the automated debugger can propose a rather small number of alternatives that include the intended program. Search space is kept small because constraints effectively prune many irrelevant alternatives. The paper demonstrates the technique by way of examples.

  • 静的解析と制約充足によるプログラム自動デバッグ

    網代 育大, 長 健太, 上田 和紀

    コンピュータソフトウェア   15 ( 1 ) 54 - 58  1998年01月  [査読有り]

  • Optimizing KLIC Generic Objects by Static Analysis

    Kazunori Ueda, Ryoji Tsuchiyama

    Proc. 11th Int. Conf. on Applications of Prolog/Prolog Association of Japan     27 - 33  1998年

    担当区分:筆頭著者

    CiNii

  • Constraint-Based Automated Debugging

    Dagstuhl Seminar (9741) on Concurrent Constraint Programming: The Next Ten Years, Schloss Dagstuhl, Germany    1997年10月

  • 静的解析と制約充足によるプログラム自動デバッグ

    日本ソフトウェア科学会第14回大会論文集   pp.533-536  1997年10月

  • 見込み計算を用いたニュースリーダの応答性改善法

    情報処理学会論文誌   38;6,pp.1235-1243  1997年06月  [査読有り]

  • 制約に基づく解析による並行論理プログラムの自動デバッグ

    人工知能学会全国大会論文集   pp.205-208  1997年06月

  • Diagnosis of Concurrent Logic Programs

    Dagstuhl Seminar (9704) on High-Level Concurrent Languages (Schloss Dagstuhl, Germany)    1997年01月

  • 制約概念に基づくプログラム解析・診断・デバッグ−並行論理型言語への適用

    日本ソフトウェア科学会大会論文集/日本ソフトウェア科学会    1996年09月

  • Diagnosing Non-Well-Moded Concurrent Logic Programs

    Proc. 1996 Joint Conference and Symposium on Logic Programming (Michael Maher (Ed.))/The MIT Press   215-229  1996年09月  [査読有り]

  • 並列計算機システムFOLON上へのPVMの移植と評価

    情報処理学会研究報告/情報処理学会   96;80 (96-ARC-119)  1996年08月

  • 並行論理プログラムのモード解析手法を用いた静的診断

    人工知能学会全国大会論文集/人工知能学会    1996年06月

  • モード誤りをもつ並行論理プログラムの静的デバッグ手法

    1996年並列処理シンポジウム論文集/情報処理学会    1996年06月  [査読有り]

  • Experiences with Strong Moding in Concurrent Logic/Constraint Programming

    Proc. International Workshop on Parallel Symbolic Languages and Systems (T. Ito, R. H. Halstead, C. Queinnec (Eds.)), Lecture Notes in Computer Science   1068   134 - 153  1996年04月

  • 並列計算機システムFOLONの通信ライブラリの設計と評価

    情報処理学会研究報告/情報処理学会   96;23 (93-ARC-117)  1996年03月

  • プログラムを書こう,プログラムを読もう

    bit/共立出版   28;1  1996年01月

  • 見込み計算を用いたネットワークニュースリーダの応答性改善法

    インタラクティブ・システムとソフトウェアIII(田中二郎編)/近代科学社    1995年11月

  • Experiences with Strong Moding in Concurrent Logic/Constraint Programming

    International Workshop on Parallel Symbolic Languages andSystems (PSLS'95, Beaune, France)    1995年10月

  • Strong Moding in Concurrent Logic/Constraint Programming

    Twelfth International Conference on Logic Programming (ICLP'95, Kanagawa, Japan)    1995年06月  [招待有り]

  • I/O Mode Analysis in Concurrent Logic Programming

    Theory and Practice of Parallel Programming (Ito, T. and Yonezawa, A., eds.), Lecture Notes in Computer Science   907   356 - 368  1995年05月

    DOI

    Scopus

    4
    被引用数
    (Scopus)
  • The Mode System of Moded Flat GHC

    Kazunori Ueda

    Guy E. Blelloch, K. Mani Chandy and Suresh Jagannathan (eds. ), Specification of Parallel Algorithms, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 18, American Mathematical Society     259 - 274  1994年

  • Moded Flat GHC and Its Message-Oriented Implementation Technique

    Kazunori Ueda, Masao Morita

    New Generation Computing   13 ( 1 ) 3 - 43  1994年  [査読有り]

    担当区分:筆頭著者

     概要を見る

    Concurrent processes can be used both for programming computation and for programming storage. Previous implementations of Flat GHC, however, have been tuned for computation-intensive programs, and perform poorly for storage-intensive programs (such as programs implementing reconfigurable data structures using processes and streams) and demand-driven programs. This paper proposes an optimization technique for programs in which processes are almost always suspended. The technique compiles unification for data transfer into message passing. Instead of reducing the number of process switching operations, the technique optimizes the cost of each process switching operation and reduces the number of cons operations for data buffering.
    The technique is based on a mode system which is powerful enough to analyze bidirectional communication and streams of streams. The mode system is based on mode constraints imposed by individual clauses rather than on global dataflow analysis, enabling separate analysis of program modules. The introduction of a mode system into Flat GHC effectively subsets Flat GHC; the resulting language is called Moded Flat GHC. Moded Flat GHC programs enjoy two important properties under certain conditions: (1) reduction of a goal clause retains the well-modedness of the clause, and (2) when execution terminates, all the variables in an initial goal clause will be bound to ground terms. Practically, the computational complexity of all-at-once mode analysis can be made almost linear with respect to the size n of the program and the complexity of the data structures used, and the complexity of separate analysis is higher only by O(log n) times.

  • Design and Evolution of the Concurrent Programming Language GHC

    早稲田大学理工学部紀要

    早稲田大学理工学部紀要   57   1 - 16  1994年  [査読有り]  [招待有り]

  • Moded Flat GHC for Data-Parallel Programming

    Proc. FGCS'94 Workshop on Parallel Logic Programming, ICOT, Tokyo   27-35  1994年  [査読有り]

    担当区分:筆頭著者

  • Message-Oriented Parallel Implementation of Moded Flat GHC

    K. Ueda, M. Morita

    New Generation Computing   11 ( 3-4 ) 323 - 341  1993年  [査読有り]

    担当区分:筆頭著者

     概要を見る

    We proposed in Ref 5) a new, message-oriented implementation technique for Moded Flat GHC that compiled unification for data transfer into message passing. The technique was based on constraint-based program analysis, and significantly improved the performance of programs that used goals and streams to implement reconfigurable data structures. In this paper we discuss how the technique can be parallelized. We focus on a method for shared-memory multiprocessors, called the shared-goal method, though a different method could be used for distributed-memory multiprocessors. Unlike other parallel implementations of concurrent logic languages which we call process-oriented, the unit of parallel execution is not an individual goal but a chain of message sends caused successively by an initial message send. Parallelism comes from the existence of different chains of message sends that can be executed independently or in a pipelined manner. Mutual exclusion based on busy waiting and on message buffering controls access to individual, shared goals. Typical goals allow last-send optimization, the message-oriented counterpart of last-call optimization. We have built an experimental implementation on Sequent Symmetry. In spite of the simple scheduling currently adopted, preliminary evaluation shows good parallel speedup and good absolute performance for concurrent operations on binary process trees.

  • The Fifth Generation Project : Personal Perspectives

    Commun. ACM   36/3,65-76  1993年  [査読有り]  [招待有り]

  • 第五世代コンピュータ技術の開花と結実に向けて

    ICOTジャーナル   34/,40-68  1993年

  • 理論と実際のギャップ:並列プログラミング

    情報処理   34/7,845-847  1993年

  • 理論は実践を導けるか,実践は理論を生かせるか?

    情報処理   33/3,272-289  1992年

  • Message-Oriented Parallel Implementation of Moded Flat GHC

    K. Ueda, M. Morita

    FIFTH GENERATION COMPUTER SYSTEMS 1992, VOLS 1 AND 2     799 - 808  1992年  [査読有り]

    担当区分:筆頭著者

  • 並列論理型言語上の制約充足方式の比較

    横尾 真, 上田 和紀

    情報処理学会論文誌   32 ( 3 ) 296 - 303  1991年  [査読有り]

     概要を見る

    本論文では 従来から提案されている制約充足問題の解法である(1)単純なバックトラック型の解法 バックトラック型の解法の改良である(2)フォワードチェック型の解法と 近年提案された並列論理型言語向きの 処理の並列性を最大限に引き出すための新しい制約充足問題の解法である(3)レイャードストリーム型の解法の比較を行うレイャードストリーム型の解法は並列に得られた途中解を併合して解を求めるという 従来の解法と非常に異なった性質を持つが その処理量 並列度に関する考察が十分なされていなかった本論文は実験的な評価と統計的モデルを用いた評価により 他の2方式との比較を行い その性質を明らかにする実験的な評価で得られた結果は統計的なモデルで示される性質とよく一致しており 以下の新しい結論が導かれた(a)弱い制約が変数間に均一に存在する問題に対して 並列に得られた途中解を併合するレィャードストリーム型の解法は 複数のプロセスが途中解を共有するため 1つの途中解を生成するための処理畳が少ない生成する途中解の個数は多いが 全体としての処理量は バックトラック型の解法よりも少なく フォワードチェック型の解法と同程度であり 処理の並列性は最も大きい(b)一方 強い制約が一部の変数間にのみ存在する問題に対して フォワードチェック型の解法は強い制約を早期に利剛しうるが レィャードストリーム型の解法は 強い制約の存在により最終的な解の一部となりえない途中解を多く生成し フォワードチェック型の解法と比較して処理量が多くなる

    CiNii

  • Design of the Kernel Language for the Parallel Inference Machine

    K. Ueda, T. Chikayama

    Computer Journal   33 ( 6 ) 494 - 500  1990年12月  [査読有り]

     概要を見る

    We review the design of the concurrent logic language GHC, the basis of the kernel language for the Parallel Inference Machine being developed in the Japanese Fifth Generation Computer Systems project, and the design of the parallel language KL1, the actual kernel language being implemented and used. The key idea in the design of these languages is the separation of concurrency and parallelism. Clarification of concepts of this kind seems to play an important role in bridging the gap between parallel inference systems and knowledge information processing in a coherent manner. In particular, design of a new kernel language has always encouraged us to re-examine and reorganise various existing notions related to programming and to invent new ones.

  • Designing a Concurrent Programming Language

    Proceedings of an International Conference organized by the IPSJ to Commemorate the 30th Anniversary (Into-Japan'90), Information Processing Society of Japan   87-94  1990年  [招待有り]

  • A New Implementation Technique for Flat GHC

    K. Ueda, M. Morita

    Logic Programming: Proceedings of the Seventh International Conference     3 - 17  1990年  [査読有り]

    担当区分:筆頭著者

  • Theory and Practice of Concurrent Systems

    ICOT Journal, Institute for New Generation Computer Techmology, Tokyo   2-42  1989年

  • 並列論理型言語GHCとそのプログラミング技術

    人工知能学会誌   4/3,258-264  1989年

  • Parallelism in Logic Programming

    Kazunori Ueda

    Information Processing 89, Ritter, G. X. (ed. ), North-Holland     957 - 964  1989年  [査読有り]  [招待有り]

    担当区分:筆頭著者

  • Theory and Practice of Concurrent Systems

    ICOT Journal, Institute for New Generation Computer Techmology, Tokyo   /23,2-42  1989年

  • 並列プログラミングとGHC

    上田 和紀

    bit   20 ( 10 ) 83 - 98  1988年10月

  • Guarded Horn Clauses: A Parallel Logic Programming Language with the Concept of a Guard

    Kazunori Ueda

    Programming of Future Generation Computers, Nivat, M. and Fuchi, K. (eds. ), North-Holland, Amsterdam     441 - 456  1988年08月

  • GHC - A Language for a New Age of Parallel Programming

    K. Furukawa, K. Ueda

    Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1988. Lecture Notes in Computer Science   338   364 - 376  1988年  [査読有り]  [招待有り]

  • Theory and Practice of Concurrent Systems : The Role of Kernel Language in the FGCS Project

    Proc. Int. Conf. on Fifth Generation Computer Systems 1988, ICOT   165-166  1988年  [招待有り]

  • Transformation Rules for GHC Programs

    Kazunori Ueda, Koichi Furukawa

    Proc. Int. Conf. on Fifth Generation Computer Systems 1988, ICOT, Tokyo   582-591  1988年  [査読有り]

  • Guarded Horn Clauses(用語解説)

    人工知能学会誌   3/1,119  1988年

  • Concurrent Prolog : Collected Papers (Volume1)

    The MIT Press, Cambridge, Mass. ,   /,140-156  1987年

  • 並列プログラミング言語GHCの設計思想

    上田 和紀

    bit   19 ( 12 ) 4 - 14  1987年

  • 並列プログラミングへのアプローチ

    上田 和紀

    通信工業   27/3,10-16  1987年

  • Making Exhaustive Search Programs Deterministic

    K. Ueda

    New Generation Computing   5 ( 1 ) 29 - 44  1987年  [査読有り]

  • Making Exhaustive Search Programs Deterministic, Part II

    Kazunori Ueda

    Proc. Fourth Int. Conf. on Logic Programming, The MIT Press, Cambridge, Mass.   356-375  1987年  [査読有り]

  • 並列プログラミング言語

    上田 和紀

    情報処理   27 ( 9 ) 995 - 1004  1986年09月  [招待有り]  [国内誌]

    担当区分:筆頭著者, 責任著者

  • Introduction to Guarded Horn Clauses

    NEC Research and Development   84   6 - 13  1986年

  • Guarded Horn Clauses

    Kazunori Ueda

    Logic Programming '85. LP 1985. Lecture Notes in Computer Science   221   168 - 179  1986年  [査読有り]

     概要を見る

    A set of Horn clauses, augmented with a ‘guard’ mechanism, is shown to be a simple and yet powerful parallel logic programming language.

    DOI

    Scopus

    53
    被引用数
    (Scopus)
  • Guarded Horn Clauses and Experiences with Parallel Logic Programming

    1986 Proc. Fall Joint Computer Conferences, IEEE Computer Society   948-954  1986年

  • Guarded Horn Clauses

    Kazunori Ueda

    D.Eng. Thesis, University of Tokyo    1986年

  • Making Exhaustive Search Programs Deterministic

    Kazunori Ueda

    Third International Conference on Logic Programming. ICLP 1986. Lecture Notes in Computer Science   225   270 - 282  1986年  [査読有り]

    担当区分:筆頭著者

    DOI

    Scopus

    7
    被引用数
    (Scopus)
  • Concurrent Prolog Compiler on Top of Prolog

    Kazunori Ueda, Takashi Chikayama

    Proc. 1985 Symp. on Logic Programming, IEEE Computger Society   119-126  1985年  [査読有り]

  • Mandala : A Logic Based Knowledge Programming System

    Koichi Furukawa, Akikazu Takeuchi, Susumu Kunifuji, Hideki Yasukawa, Masaru Ohki, Kazunori Ueda

    Proc. Int. Conf. on Fifth Generation Computer Systems ICOT, Tokyo     613 - 622  1984年  [査読有り]

  • What Is a Variable in Prolog?

    Nakashima, H, Tomura, S, Ueda, K

    Proc. Int. Conf. on Fifth Generation Computer Systems 1984, ICOT, Tokyo     327 - 332  1984年  [査読有り]

  • Efficient Stream/Array Processing in Logic Programming Languages

    Kazunori Ueda, Takashi Chikayama

    Proc. Int. Conf. on Fifth Generation Computer Systems 1984, ICOT, Tokyo     317 - 326  1984年  [査読有り]

  • 述語論理型言語における副作用によらない入出力と文字列操作

    中島 秀之, 上田 和紀, 戸村 哲

    情報処理学会論文誌   24 ( 6 ) 745 - 753  1983年  [査読有り]

     概要を見る

    Prologに代表される述語論理型言語は プログラムを その仕様に近い形で記述できることを大きな特徴とする.しかし入出力に関しては 命令型言語と同様 副作用を通じて行うことが多かった.本論文では 述語ではなく変数を通じた 副作用によらないPrologの入出力を論じる.また従来の多くの言語の入出力は データの転送と 内外部表現間の変換を まとまった機能として提供していた.本論文では 入出力はたんなる文字列の転送ととらえ 変換操作は 言語に文字列操作機能を用意し それを用いて記述するようにした.これらの工夫により 入出力の概念が単純でわかりやすいものになり しかもその扱いが柔軟になったと考える.順アクセス媒体との入出力は たんなる文字列変数を通じて行えばよいが データ構造の工夫により 窓構造をもったディスプレイヘの出力も扱える.文字列操作は Prologのパターンマッチング機能を用いて簡潔に記述できる.実行可能パターンの考え方をとりいれてパターンと述語とを統一的に扱うので 文字列に導入した基本操作が連結のみであるにもかかわらず パターンの記述能力は強力である.提案する機能はProIog/KR上に作成中であるが さらに効率のよい作成技法にもふれる.残された課題には 複雑なパターンマッチングにおけるバックトラックの制御などがある.

    CiNii

  • Binary Decision Treeによる多重分光画像の高速処理

    稲村 実, 豊田 弘道, 上田 和紀, 大森 隆司, 藤村 貞夫

    計測自動制御学会論文集   5/4,486-491  1979年  [査読有り]

▼全件表示

書籍等出版物

  • AI事典 第3版

    ( 担当: 分担執筆,  担当範囲: 1.2「第五世代コンピュータ」(pp.4-5))

    近代科学社  2019年12月

  • 人工知能学大事典

    ( 担当: 分担執筆,  担当範囲: 5-12「論理プログラミング」(pp.243-244))

    共立出版  2017年07月

  • Programming Languages and Systems 8th Asian Symposium, APLAS 2010

    Kazunori Ueda (ed.)

    Lecture Notes in Computer Science 6461, Springer-Verlag  2010年

  • 人工知能学事典

    人工知能学会編

    共立出版  2005年12月

  • Functional and Logic Programming-5th International Symposium on Functional and Logic Programming, FLOPS 2001

    Herbert Kuchen and Kazunori Ueda (eds.)

    Lecture Notes in Computer Science 2024, Springer-Verlag  2001年

  • Advances in Computing Science: ASIAN '97

    R.K. Shyamasunder and Kazunori Ueda (eds.)

    Lecture Notes in Computer Science 1345, Springer-Verlag  1997年

  • 並列処理シンポジウムJSPP'97論文集

    情報処理学会  1997年

  • 楽しいプログラミング:記号の世界

    中島秀之, 上田和紀

    岩波書店  1992年

  • Logic Programming : Proceedings of the 1991 International Symposium

    Vijay Saraswat and Kazunori Ueda (eds.)

    The MIT Press  1991年

  • 続・新しいプログラミング・パラダイム

    井田哲雄, 田中二郎編, 上田和紀他共著( 担当: 共著,  担当範囲: 第1章 "並行プログラミングとGHC" (pp.1-34))

    1990年11月

  • 知的コンピュータシステム事典

    ( 担当: 分担執筆,  担当範囲: 2.1.4(1) 「Concurrencyと並列性」)

    産業調査会 事典出版センター  1989年08月

  • 並列論理型言語GHCとその応用

    淵一博監修, 古川康一, 溝口文雄共編, 古川康一, 竹内彰一, 上田和紀, 他, 名共著( 担当: 共著,  担当範囲: 第3章 "GHCの基本" (pp.33-66),第5章 "GHCによる全解探索" (pp.93-115),付録 "GHCのProlog上の処理系" (pp.217-270))

    1987年09月

  • プログラム言語 Ada: 基準文法書解説

    上田 和紀( 担当: 共著,  担当範囲: pp.87-128)

    bit 臨時増刊,共立出版  1981年10月

▼全件表示

Misc

▼全件表示

Works(作品等)

  • 制約概念に基づくハイブリッドシステムモデリング言語HydLa

    ソフトウェア 

    2010年
    -
    継続中

  • LMNtal: モデル検査機能と可視化環境を備えた階層グラフ書換え言語処理系

    ソフトウェア 

    2002年
    -
    継続中

受賞

  • フェロー

    2016年   日本ソフトウェア科学会  

  • フェロー

    2015年   情報処理学会  

  • 基礎研究賞

    2011年   日本ソフトウェア科学会  

  • 日本ソフトウェア科学会第5回論文賞

    2001年  

  • 日本ソフトウェア科学会第4回論文賞

    2000年  

  • 第7回日本IBM科学賞

    1993年  

  • 第3回元岡賞

    1988年  

  • 功労賞

    2010年   日本ソフトウェア科学会  

  • 人工知能学会2002年度全国大会ベストプレゼンテーション賞

    2003年  

  • 日本ソフトウェア科学会第19回高橋奨励賞

    2002年  

  • 情報処理学会第30回全国大会学術奨励賞

    1985年  

  • 日本ソフトウェア科学会第2回高橋奨励賞

    1985年  

▼全件表示

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

  • 先進的プログラム構築方法論に支えられた高機能な3D印刷造形技術の開拓

    科学研究費挑戦的研究(萌芽)

    研究期間:

    2018年06月
    -
    2021年03月
     

     概要を見る

    初年度は,熱可塑性樹脂を用いた積層型3D印刷による高機能造形物実現のための基礎固めを目標に,以下の研究開発(一部準備作業を含む)を実施した。<BR>(1) 3Dプリンタ,樹脂素材,スライサの特性理解: 開発する技術の再現性の担保のためには,ハードウェア,材料,ソフトウェアの三者それぞれについて利用経験を積み,特性ないし癖を把握してノウハウを蓄積することが重要である。そこで,現有の3Dプリンタ1機種3台に加えて2機種4台を新たに導入し組み立てるとともに,数種類のスライサソフトウェアと多様な材料で多くの印刷実験を行った。またこれを通じて,素材および造形物の強度,サポート材なしの印刷におけるブリッジ耐性やオーバーハング耐性などについての検討を進めた。これを通じて,目標として掲げていた「適切な部材組合せに必要な0.05mm前後の寸法精度の安定確保」の見通しを得た。(2) 機能部品の設計技術: 3D印刷の部品化概念の開拓の第一歩として,梁のような細長い部品を強固に相互接続する方法の実験的検討を進めた。日本の伝統建築に見られる継手の中から,主に追掛け大栓継ぎと尻掛け継ぎの超小型版について試作を重ね,断面が3mm×6mm程度の部材でも十分強固に接続できる見通しを得た。また,3D積層印刷による弾性機能実現にとって有利な形状とは言えないコイルばねの印刷について,実用性確認のための基礎実験を重ねた。<BR>研究代表者自身による上記の実験に加え,機械工学を専門とする研究協力者および大学院生との定期的な会合を設け,通常の積層にとどまらないさまざまな技法について検討および情報交換を行った。また3D印刷の展示会の参加等を通じて最新技術の調査を行った。7月からの研究は実験設備の導入,組み立て,整備から始まったため,実質的な研究期間は限られていたが,その中で機械と材料についての知見とノウハウの蓄積を進めることを最優先に研究を進めた。現場的な観点からの経験は深まったが,これを工学につなげるのはこれからである。<BR>当初想定していなかった知見として,既存の数種類のスライサソフトウェアの機能とその限界を知ることができた。つまり,通常のスライサは多様なパラメタ設定が可能であるが,3Dプリンタの制御を自由にプログラムすることはできない。このことから,高度な3D印刷のためのソフトウェア開発は,印刷物表現の標準形式であるSTLではなく,3Dプリンタの制御言語であるGコードをインタフェースとして進める必要があるとの知見を得た。当初の研究計画のとおり,機能部品の設計技術よび部品の組合せ技術を中心とした研究開発を進めるが,以下の点に留意する。<BR>1. 第一年度に得られた上記の知見に基づき,ソフトウェアについては,低レイヤすなわちGコードレベルの技術の調査および開拓を優先させる。2. 2次元印刷をZ軸方向にヘッドを単調移動させながら繰り返すという従来手法とらわれずに,真の3次元印刷技術の可能性の探求に着手する。3. ソフトウェア技術の開拓を行いつつ,得られた知見のデータベースの作成にも取り組む

  • プログラミング言語技術との融合による高水準モデリング言語の進化と展開

    科学研究費基盤研究(B)

    研究期間:

    2018年04月
    -
    2021年03月
     

     概要を見る

    プログラミング言語技術との融合による高水準モデリング言語とその処理系の進化を目標に,グラフ構造を扱うLMNtalおよび実数を扱うHydLaの二つのモデリング言語について以下の研究開発を実施した。<BR>グラフ書換え言語LMNtalについて,以下の新言語機能の設計と実装を行った。(1)全称量化子を伴うグラフパターンマッチングの意味論を定め,仮想機械での実装を実現し例題記述を行った。(2)λ計算の簡約を簡潔に記述するための新たなグラフ型を提案し実装した。(3)モデル検査における並行プロセスの自動抽象化技法能を提案し,正当性を証明し実装を行った。また正当性証明のためにLMNtalの操作的意味論の検討と整備を行った。(4)LMNtalグラフの既存の型概念を検討して再定式化を行った。(5)グラフのための内包表記の検討を進めた。(6)非決定実行インタプリタの記述を可能にするAPIを定めて公開した。LMNtal実行・検証系については,集中作業合宿を実施してC++化による可読性・保守性の改善作業を行うとともに,LMNtalモデル検査器の要素技術となるグラフ差分を利用した効率的グラフ正規化技法の処理系への組み込みを進めた。<BR>制約概念に基づくハイブリッドシステムモデリング言語HydLaについては,言語機能と実装技法について以下の研究開発を行った。(1)変数および制約階層の動的生成のための記法を定めて実装を行った。(2)シミュレーション中の制約処理過程を動的に解析して再利用する技法の開発を行った。(3)モデル抽象化技法を実行性能改善に応用する技法を開拓した。(4)記号パラメタをもつ非線形常微分方程式の精度保証近似解法の開発と評価を行った。(5)微分代数方程式の求解性能向上方法の検討を進めた。(6)集中検討合宿を行って,オープンソース制約エンジンの有力候補となるSageMathの評価検討を行った。研究開発のコアとなる二つのモデリング言語の言語機能と実装技法について,多岐にわたる要素技術の開拓を進めることができた。これには,年度末時点では設計の詰めの段階で初回の学会発表を行ったばかりのものも一部含まれるが,多くは試験実装を経て評価・改良中,またはGithubで公開中の処理系の主たるブランチにすでに反映済みである。<BR>研究分担者および連携研究者との交流も進め,フランス・ナント大学の制約プログラミング研究グループとも相互訪問を行った。プログラミングおよびモデリング言語の研究開発における理論と実践の強い連携という基本方針に基づいて,育ってきた要素技術を発展させてGithubから公開中のモデリング言語実行・検証系に統合する作業を推進する。<BR>LMNtalとその処理系については,(1)言語機能としてほぼ確立できた高階概念の本格実装および応用の展開,(2)グラフのための強力な型体系の,グラフの型検査からグラフ書換え規則の型検査への発展,(3)全称量化グラフパターンにマッチしたグラフの書き換えのための構文,意味論,実装の整備,などを進める。<BR>HydLaとその処理系については,特に(1)処理系の基礎をなす操作的意味論と言語仕様の根幹をなす宣言的意味論の整合性の検討,(2)プログラムの等価性のより深い検討およびそれを支える精密な意味論の整備,(3)プログラム変換技法の開発とその実行最適化への応用,(4)制約エンジンの求解能力および性能向上,などを進める

  • 実数と時間の概念を備えた汎用高水準プログラミング言語

    科学研究費挑戦的萌芽研究

    研究期間:

    2015年04月
    -
    2018年03月
     

     概要を見る

    サイバーフィジカルシステムにおける計算とプログラミングの基盤の確立に向けて,連続量と時間を的確に扱うことのでき汎用の高水準プログラミング言語が備えるべき言語要素と意味論の詳細検討を推進した.目標とする言語は並行処理や通信機能を有する並行プログラミング言語であり,かつ連続量とその不確定性を扱うことのできる制約プログラミング言語でもあるという作業仮説に立ち,既存の言語に対する詳細検討を通じて,(1) 制約階層概念とその意味論,(2) 時間概念,(3) データ領域,(4) 動的に進化する並行系の記述,の各側面を中心に,目標とする言語の理論基盤と備えるべき機能の多くを明らかにした

  • 検証系を備えた高水準モデリング言語処理系の実装技術の深化

    科学研究費基盤研究(B)

    研究期間:

    2014年04月
    -
    2017年03月
     

     概要を見る

    本研究では,実数やグラフ構造など,高い抽象性と汎用性をもつ情報表現を扱う高水準モデリング言語の実装技術の深化に取り組んだ.連続変化と離散変化の両方をもつハイブリッドシステムの高信頼シミュレーションのために,精度保証付き数値計算技術と記号処理との統合手法などを開拓し,制約概念に基づくモデリング言語HydLaの記号シミュレータの求解能力と実行効率を大きく改善した.また,グラフ書換えモデリング言語LMNtalの実行系について,ハイパーグラフ書換えへの発展,並列モデル検査アルゴリズムの改善等を行い,より強力な検証ツールへと発展させた.開発した処理系はオープンソースソフトウェアとして公開した

  • 検証技術と非標準型体系を用いたモデル検査器コンパイラの進化的発展

    科学研究費挑戦的萌芽研究

    研究期間:

    2012年04月
    -
    2015年03月
     

     概要を見る

    非手続き型高水準言語の適用分野として,さまざまな系のモデリングと検証が今後重要性を増すと期待される.研究代表者らはモデル検査機能を通常の計算と同一の枠組で提供するグラフ書換え言語処理系の開発と公開を進めてきたが,コンパイラの進化的発展と信頼性確保が課題であった.本研究では,コンパイラと実行時処理系をつなぐ抽象機械によるグラフ書換え操作の形式化と検証を行うことで,コンパイラの検証に向けた一歩を踏み出した.また,モデルの解析,理解,最適化に役立つグラフ書換え言語のための新たな型体系を,微視的な接続関係に着目した体系とグラフ全体の形状を扱う体系の両面から検討してそれぞれ構築した.

  • 高性能検証系を統合した高水準モデリング言語処理系の構築

    科学研究費基盤研究(B)

    研究期間:

    2011年04月
    -
    2014年03月
     

     概要を見る

    自然系や記号系,および両者が混在するサイバーフィジカルシステムのモデリングと検証技術は今後ますます重要性を増すと期待される.本研究では,グラフや集合,方程式や不等式といった,情報学の枠にとどまらない高度に一般的な概念に基づく高水準モデリング言語とそれを用いた検証技術の可能性を,実行系と検証系を統合した複数の処理系を具体的に構築することによって示した.本研究開発によって,グラフ書換え言語LMNtalの処理系はハイパーグラフ書換え機能を備えた並列モデル検査器へと進化し,ハイブリッド制約言語HydLaの処理系は不確定性をもつハイブリッドシステムの非決定的記号実行系へと進化した

  • 制約最適化問題のSAT変換による解法とその並列分散処理に関する研究

    科学研究費基盤研究(A)

    研究期間:

    2008年
    -
    2012年
     

     概要を見る

    制約充足および最適化問題に対するSAT技術と,その並列分散実装に関する研究を進め, 105件の雑誌論文公表, 67件の学会発表を行った.また,世界をリードするソフトウェアを開発した. 2008年と2009年のCSPソルバー競技会グローバル制約部門優勝のSugar, 2011年SAT競技会応用UNSAT部門優勝のGlueMiniSat, 2010年と2011年のMax. SAT競技会部分Max. SAT応用部門優勝のQMaxSAT

  • 高水準ハイブリッド制約モデリング言語とその高信頼実装

    科学研究費基盤研究(B)

    研究期間:

    2008年
    -
    2011年
     

     概要を見る

    連続変化と離散変化の両方を有するハイブリッドシステムの高信頼シミュレーションと検証のための高水準モデリング言語HydLa を設計し,その宣言的意味論と実行方式を確立させた.HydLaは数学および論理学の記法を利用した宣言的記述,制約概念を活用した不確定情報の扱い,簡潔な記述のための制約階層化機能などを特徴とする.また,不確定情報の存在下でのシミュレーションや検証の正当性を確保するために離散変化の区間求解アルゴリズムを確立するとともに,HydLaの主要機能を備えた統合試作処理系を構築した

  • 情報爆発に対応する高度にスケーラブルなソフトウェア構成基盤

    科学研究費特定領域研究

    研究期間:

    2006年
    -
    2011年
     

     概要を見る

    爆発的に増加する大量の情報を効率的に扱うソフトウェアの構成には、広域に分散配置した高度な並列性を持つ情報システムを柔軟に記述できるソフトウェアの枠組が基本技術として必要となる。このためのプログラミング言語やミドルウェアのシステムと、複雑なソフトウェアの正当性を検証するためのシステムを対象に研究を進め、具体的なシステムを提案、設計、実装し、その性能を検証した。代表的成果ソフトウェアは公開している

  • 計算機科学における離散と連続に関する調査と新しい展開

    科学研究費基盤研究(C)

    研究期間:

    2006年
    -
    2007年
     

     概要を見る

    特定領域研究を申請するために3回の会議を開催した。5月27日には名古屋で「自然計算における離散と連続」、7月15日には東京で「自然計算における理論と実証」、9月2日には東京で「申請に向けて」、である。特定領域研究「自然計算--構成的アプローチの実証とその理論--」を11月に無事に申請した。さらに、今後のこの分野を概観するための第4回会議を3月24日に東京で開催した。本基盤研究(C)の成果の第1は特定領域研究「自然計算--構成的アプローチの実証とその理論--」の企画・申請である。次に、基盤研究(C)を申請した段階では、自然計算を理解する問題を離散と連続の間の問題であると矮小に捕らえていたのだが、特定領域研究の申請段階では、ハイブリッド的確率的多体的システムに対する計算論として自然計算を理解するようになった。これが、基盤(C)の調査研究としての側面の具体的な成果である。現存しないハイブリッド的確率的多体的システムの計算論の必要性を、構成的材料工学と合成生物学に対する応用と新しい理論情報科学分野の開拓という両面から訴えたのが特定領域研究「自然計算--構成的アプローチの実証とその理論--」である。離散性と連続性の問題であるハイブリッド性の他に、自然の持つ揺らぎと超分散性を自然計算の基本要素であると理解し、これらの性質を持つシステム上の計算論の構築とその応用を研究分野として申請した

  • 構造的分子計算理論-自律的計算系の解析と設計のための基礎理論

    科学研究費特定領域研究

    研究期間:

    2006年
    -
    2007年
     

     概要を見る

    (1)膜計算モデルにおける新しい計算モデルの提案:神経細胞系をモデルとして,膜計算の新しいモデル「Spiking Neural P-Systems」を提案し,受理器と生成器の両タイプにおいてその計算能力の万能性を示した。
    (2)平衡状態の効率の良い計算手法の開発:入力分子のサイズに比して会合の結果生成される分子複合体の個数が組合せ論的な爆発をするような反応系に対して,平衡状態を計算するための一般論を構築した。平衡状態計算を系全体の自由エネルギーの最小化問題として定式化し,変数の個数を著しく削減する新しいアルゴリズムを開発した。
    (3)細胞並列計算に向けたバクテリアセルオートマトンの実装:細胞を用いたセルオートマトンの実現に向けての第一歩として,細胞内分子反応メカニズムを用いて自律的でプログラム可能なバクテリアコンピュータを開発した。これは世界で初めてバクテリアを用いて計算が実行できたことを証明するものである。
    (4)抽象化学反応計算モデルの研究:微分方程式系などでは解析が困難な少数分子の化学反応系の振る舞いについて計算機実験と数理的解析により検討し,特にBelousov-Zhabotinsk (BZ)反応の数理モデルであるBrruselatorとOregonatorについて,分子数が少数になることによる不安定性について解析した。
    (5)分子計算シミュレータ:階層構造と接続構造の両方を扱う階層グラフ書換えモデルLMNtalの表現力検証のために,代表的計算モデルのエンコード法の確立と実装を行った。Ambient計算のエンコードにおいては自己調整に基づく分散名前管理方式を実現した。純粋λ計算のエンコードにおいては,膜を活用することで従来手法よりもはるかに簡潔な方法を実現した。

  • スケーラブル統合プログラミング言語モデルLMNtalの実用化

    科学研究費基盤研究(B)

    研究期間:

    2004年
    -
    2007年
     

     概要を見る

    LMNtal(elementalと発音)は,多重集合や並行処理やモビリティなどの概念を持つさまざまな計算モデルを簡明な形で統合することを目的として,研究代表者と研究分担者が提案したプログラミング言語モデルである.本研究は,階層グラフ書換え型の計算モデルとして確立しつつあったLMNtalを実用プログラミング言語に成長させるために必要な言語機能を設計し,実装技術を確立し,実際に処理系を構築して広く公開することを目標に推進した.本研究によって得られた主要成果は以下の通りである.(a)プログラミング言語としてのLMNtalの確立-階層グラフ書換えモデルに対して,基本データ型と基本演算,モジュールシステム,他言語インタフェースなどの導入方法を検討設計し,それらを用いて多様なライブラリの構築を行った.(b)実装技法の確立と処理系の作成-LMNtal用中間言語へのコンパイラと,中間命令列を実行をつかさどる実行時処理系からなる処理系を構築した.特に,複数タスクを用いた非同期実行方式を設計・実装するとともに,逐次実行最適化機能や中間言語からJavaへのトランスレータも実装した.またグラフ自動整形機能をもつ実行可視化機能を設計・実装した.(c)記述能力の検証-LMNtalの基本的記述能力の検証のために,π計算,Ambient計算,λ計算,CHR(Constraint Handling Rules)など,多様な計算モデルをLMNtalでエンコードして,開発した処理系上で動作確認を行った.開発した処理系の規模は約5万行で,http://www.ueda.info.waseda.ac.jp/lmntal/から公開している

  • 構造的分子計算理論-自律的計算系の解析と設計のための基礎理論

    科学研究費特定領域研究

    研究期間:

    2002年
    -
    2006年
     

  • 計算連続体に基づくソフトウェア実現法

    科学研究費特定領域研究

    研究期間:

    2001年
    -
    2006年
     

     概要を見る

    本研究では,計算機システムが備えている広域性と局所性の両方に対応できる適切な計算量モデルとソフトウェアシステムの構築を可能にするために,計算連続体と呼ぶ概念に基づいて,さまざまな観点から,計算に関する既存概念の再検討,統合,および発展を図ってきた.主要な研究成果は次のとおりである.1.計算連続体モデルによる計算量解析本プロジェクトでは,単一計算機内のメモリ階層から計算機間のネットワーク遅延の差異までを,統一的に,かつ簡潔に表現できる計算量モデルとして「計算連続体モデル」を提案し,このモデルに基づいた計算量解析結果が,従来方法よりも現実の計算に近いものであることを示した.また,複雑な並列アルゴリズムに対しても,その振舞いが把握できるように,計算連続体モデルの仮想機械を設計し,実装した.2.並行言語モデルLMNtalに関する研究また本プロジェクトでは,階層グラフの書換えに基づくスケーラブルな並列言語モデルとしてLMNtalを設計し,このモデルの改良を進めてきた.このモデル上でプロセス構造の解析技術を確立するとともに,実用に供するプログラミング言語としての実装を行った.階層グラフ書換えは,多重集合書換え計算モデルや自己組織化に基づく計算モデルなどを特別な場合として含んでおり,既存の多くの計算モデルの架け橋となることが期待できる.3.局所性を重視した処理系実装方式の研究プログラミング言語の実装において,特に局所性を重視することによって,実行性能が飛躍的に向上することを実証した.その例として,階層的グループ化に基づくコピー型ごみ集めによる局所性改善をあげることができる.これは,スタック溢れに備えたキューを併用することにより,少量のスタックで大部分を深さ優先順にコピーするごみ集め方式のさらなる改良の提案であり,仮想記憶の局所性だけでなく,キャッシュの局所性も考慮した実装となっており,実際の計算機上で極めて効率の良い処理系を実現できる技術である

  • 並行論理プログラミングに基づく広域分散計算パラダイムの構築

    科学研究費基盤研究(C)

    研究期間:

    1999年
    -
    2002年
     

     概要を見る

    並行論理プログラミングは,論理プログラミングに情報の流れを制御するための同期機構を導入し,並行処理記述のためのプログラミング・パラダイムとしたものである.これまでの並行論理型言語の研究開発は,主として並列計算機上での高速実行を目標に行なわれてきた.一方,コンピュータネットワークの急速な普及と共に,広域分散計算環境で稼働する効率的で安全な分散型アプリケーションを容易に構築するための方法論の確立が急務となっている.そこで本研究では(1)非均質な計算環境下での宣言型プログラミング(2)静的解析技術に基づく安全な広域分散ソフトウェア構築の両面から,並行論理プログラミングに基づく広域分散計算のための技術開発を行なった.主要成果は以下の通りである.1.シームレスな分散実行環境の構築-不均質な計算ノード上で動作する複数のKL1言語処理系をソケットを通じて透過的に接続するために,ネットワーク透過的な分散論理変数(単一代入チャネル)の技術要件および実装方式を検討し実現した.また分散論理変数に対する名前付けとその解決を行なうネーミングサービスを実現した.さらに,分散環境で不可欠となる例外処理機構の設計と実装を行った.2.分散実行環境における記憶管理-複数の変数によるデータ共有を静的に解析するための広義型体系である線形性体系を設計,実装した.さらに,並行論理プロセスの実行を資源のやり取りの観点からとらえ直し,動的記憶管理が不要なプログラムのクラスとそれを特徴づける静的型体系(capability system)を設計し,既存のモード体系と線形性体系とを一般化した形で統合した.3.コード移送を実現するためのインタプリタ構築技術-分散処理系における述語コード移送を実現するために,treecodeと呼ばれる中間コード形式を設計し,またそのインタプリタをFlat GHCで記述した.これらを通じて,並行論理型言語をベースに簡明な広域分散プログラミング・パラダイムを構築するための要素基盤を,理論と実装の両方を含む幅広い側面から与えることができた

  • 発展可能ソフトウェアの構築方法論の研究

    科学研究費重点領域研究

    研究期間:

    1997年
    -
    2000年
     

     概要を見る

    1.通信相手を特定しないオブジェクト間の通信モデルを導入し、開放分散系におけるソフトウェアの発展的な変更や拡張を効率的に行うことを可能にした。2.オブジェクトの原始プログラムの計量を行い、クラスの行数、メソッド数などの頻度分布は負の2項分布に従うことなどのオブジェクトの進化パターンを抽出した。3.仕様を代数仕様言語CafeOBJを用いてモジュール化し、それらの合成によって全体の仕様を構成する方法により、合成のパターンを再利用可能な形に分類した。4.事例研究を通して、モデル形成の過程および形式仕様の構成と記述の過程を分析し、システム仕様記述の発展過程について形式仕様記述の特徴や意義を考察した。5.並行論理プログラミングにおける強モード体系を基礎として、仕様なしでプログラムの軽微な誤りの箇所を同定し、さらに誤りを自動修正する枠組みを提案した。6.システム要求を命題述語と述語論理に基づいて定義し、これを動作モデルとなる形式仕様(状態遷移システム)に変換する方法を提案し、その健全性と完全性を証明した。7.マルチプロセス、マルチスレッドの環境で稼動し、フィールド機構のマイグレーション機能をもつマルチエージェントシステム記述用言語の開発を行った。8.「細胞に基づくプログラミング」、さらにπ計算を基盤とした「能動形プログラミング」を提案し、効率の良い実装のための可変回路部をもつJavaプロセッサLSIを開発した。9.データ構造の分散化(分散データ構造)に着目し、いくつかの異なる観点から分散データ構造の性質の解明とその効率のよい実装法の開発を行った

  • 広域情報の実時間アクセスのためのアーキテクチャとソフトウェア

    並列・分散処理研究推進機構 

    研究期間:

    1997年
    -
    2000年
     

  • 並行論理プログラミングにおける静的モード体系の応用的側面に関する研究

    科学研究費基盤研究(C)

    研究期間:

    1995年
    -
    1998年
     

     概要を見る

    GHC(Guarded Horn Clauses)をはじめとする並行論理プログラミング言語は、簡潔な通信・同期機構と柔軟な記述力とを特徴とするが、その実用化を図るには、プログラミング支援と処理効率の両面から、プログラムの静的解析技法がきわめて重要となる。研究代表者はこれまでに、GHCプログラムの情報の流れ(モード)を論じるためのモード体系と、静的モード解析技法を提案し、その理論的側面を整備してきた。本研究では、この静的モード体系に対し、新たに応用的側面から検討を加え、その有用性をさまざまな角度から実証した。1. モード解析システムの実装-並行論理型言語KL1のためのモード解析システムklintを、KL1言語自身で実装した。現実のプログラムに適用することによってシステムの評価・拡充を繰返し、複雑なKL1プログラムに対応できる実用的なシステムとした。2. モード体系の下での記述能力の検証-klintシステム自身をはじめとする実用規模の並行論理プログラムの解析を通じ、静的モード体系を備えた並行論理型言語の記述力が十分であることを明らかにした。3. デバッグへの応用-モード体系はプログラムの誤りの静的検出にも非常に有効である。そこで、モードづけできないプログラムの誤りを効率よく解析するアルゴリズムを提案し、実装を行なった。本技法は制約に基づく静的体系一般に適用可能なものとなった。さらにプログラム誤りの自動修正の方法を提案し、その修正能力を確認した。4. 静的モード体系を利用した処理系の改善-モード解析情報に、データ型やデータ参照数についての解析情報を併用することにより、タグ判別をはじめとする動的な判断の多くが省略でき、手続き型言語で直接記述した場合と大きく変わらない性能が得られることを明らかにした

  • 統合並列処理に関する研究

    IPA(情報処理振興事業協会)  創造的ソフトウェア育成事業

    研究期間:

    1996年
    -
    1997年
     

▼全件表示

講演・口頭発表等

  • 言語をつくる

     [招待有り]

    日本ソフトウェア科学会第35回大会 (August 29-31, 2018, 大阪大学)  

    発表年月: 2018年08月

  • Logic/Constraint Programming and Concurrency: The Hard-Won Lessons of the Fifth Generation Computer Project

     [招待有り]

    Thirteenth International Symposium on Functional and Logic Programming (FLOPS 2016, March 4-6, 2016, Kochi, Japan)  

    発表年月: 2016年03月

  • Hierarchical graph rewriting as a unifying model and language of concurrency

     [招待有り]

    LIX Colloquium on Emerging Trends in Concurrency Theory (November 2006, Ecole Polytechnique de Paris, France)  

    発表年月: 2006年11月

  • LMNtal: a unifying declarative language

     [招待有り]

    Third Workshop on Constraint Handling Rules (CHR 2006, July 2006, Venice, Italy)  

    発表年月: 2006年07月

  • Constraint-Based Concurrency and Beyond

     [招待有り]

    Algebraic Process Calculi: The First Twenty Five Years and Beyond (August 1-5, 2005, Bertinoro, Italy)  

    発表年月: 2005年

  • LMNtal: a language model with links and membranes

     [招待有り]

    Fifth Workshop on Membrane Computing (WMC5, June 2004, Milano, Italy)  

    発表年月: 2004年06月

  • Resource-Passing Concurrent Programming (advanced tutorial)

     [招待有り]

    Seventeenth International Conference on Logic Programming (ICLP'01, Novermber-December 2001, Paphos, Cyprus)  

    発表年月: 2001年11月

  • Resource-Passing Concurrent Programming

     [招待有り]

    Fourth International Symposium on Theoretical Aspects of Computer Software (TACS 2001, October 2001, Sendai, Japan)  

    発表年月: 2001年10月

  • Strong Moding in Concurrent Logic/Constraint Programming (advanced tutorial)

     [招待有り]

    Twelfth International Conference on Logic Programming (ICLP'95, June 1995, Kanagawa, Japan)  

    発表年月: 1995年06月

  • Designing a Concurrent Programming Language

     [招待有り]

    International Conference organized by the IPSJ to Commemorate the 30th Anniversary (InfoJapan'90, October 1990, Tokyo, Japan)  

    発表年月: 1990年10月

  • Paralleism in Logic Programming

     [招待有り]

    IFIP 11th World Computer Congress  

    発表年月: 1989年08月

  • Theory and Practice of Concurrent Systems (panel)

    Ehud Shapiro, William J. Dally, Geoffrey C. Fox, Carl Hewitt, Robin Milner, Kazunori Ueda, David H.D. Warren  [招待有り]

    International Conference on Fifth Generation Computer Systems 1988 (FGCS'88, November 1988, Tokyo, Japan)  

    発表年月: 1988年11月

  • Concurrent Logic Programming Languages (tutorial)

     [招待有り]

    Fourth International Conference on Logic Programming (ICLP'87, May 1987, Melborne, Australia)  

    発表年月: 1987年

  • Guarded Horn Clauses

     [招待有り]

    Workshop on Foundations of Logic and Functional Programming (December 1986, Trento, Italy)  

    発表年月: 1986年12月

  • Teaching (Constraint) Logic Programming

    G. Gupta, M.V. Hermenegildo, U. Nillson, P. Stuckey, K. Ueda  [招待有り]

    Ninteenth International Conference on Logic Programming (ICLP'03, December 2003, Mumbai, India)  

    発表年月: 2003年12月

  • The Future of Logic Programming (panel)

    International Logic Programming Symposium (ILPS'91, San Diego, U.S.A.)  

    発表年月: 1991年11月

▼全件表示

学内研究費(特定課題)

  • 高水準モデリング言語の特性を活かす高機能な実行・検証系

    2021年  

     概要を見る

    研究代表者らは,LMNtalおよびHydLaという二つのモデリング言語の研究開発を推進している.LMNtalはグラフ(ネットワーク)構造の変化を扱う計算モデル,HydLaは連続変化と離散変化の双方を許す実数関数を制約式で定義する計算モデルに基づいており,それぞれ多くの独自機能を備えている.また,いずれの処理系も,モデルのシミュレーションだけでなくモデル検査器(検証系)の機能を備えている点を大きな特徴とする.本研究ではこれらの言語と処理系の有用性をさらに高めるべく,LMNtalについては静的および動的な型の概念の設計と実装,ハイパーグラフを扱うための形式意味論の整備などを行った.HydLaについては検証系としての機能を高めるためのハイブリッドオートマトンモデルの導出の研究を進展させた.

  • 高水準モデリング言語の高機能な実行・検証系

    2021年  

     概要を見る

    研究代表者らは,LMNtalおよびHydLaという二つのモデリング言語の研究開発を推進している.LMNtalはグラフ(ネットワーク)構造の変化を扱う計算モデル,HydLaは連続変化と離散変化の双方を許す実数関数を制約式で定義する計算モデルに基づいており,それぞれ多くの独自機能を備えている.また,いずれの処理系も,モデルのシミュレーションだけでなくモデル検査器(検証系)の機能を備えている点を大きな特徴とする.本研究ではこれらの言語と処理系の有用性をさらに高めるべく,LMNtalについては静的および動的な型の概念の設計と実装,ハイパーグラフを扱うための形式意味論の整備などを行った.HydLaについては検証系としての機能を高めるためのハイブリッドオートマトンモデルの導出の研究を進展させた.

  • モデリング言語とその実装への高水準プログラミング言語概念の導入

    2017年  

     概要を見る

    研究代表者はグラフと実数という汎用性の高いデータを扱うモデリング言語の設計と実装に取り組み,モデリング言語LMNtalとHydLaの実行系と検証系を開発・公開してきた.本研究では,高階概念,抽象化,メタプログラミングなど,プログラミング言語分野での有用性が広く認められている概念をモデリング言語に導入するための技術課題に設計から実装まで取り組み,高信頼ソフトウェアのためのより高水準なモデリング環境の実現を目指した.成果として,グラフ書換え言語LMNtalにおいては高階関数の表現と操作,ハイブリッド制約言語HydLaにおいては変数や制約の動的生成などのさまざまな拡張を達成した.

  • ハイブリッド制約モデリング言語の高信頼実装技術

    2007年   石井 大輔

     概要を見る

    ハイブリッド制約モデリング言語とは,時間の経過に伴って状態が連続変化したり,状態や方程式系自体が離散変化したりするハイブリッドシステムを,制約 (constraints) 概念に基づいて記述・シミュレーション・検証するための高水準言語である.1990年代に先駆となる言語 Hybrid CC が提案実装されていたが,言語機能と実行結果の信頼性の両面で研究の進展が待たれていた.本研究は,新たなハイブリッド制約モデリング言語 Hydra の確立に向けて,その設計論と,計算結果の正しさを保証する高信頼実装の要素技術を開拓することを目標に実施した.本年度の成果は以下のようにまとめることができる.1. 既存のハイブリッド制約言語である Hybrid CC の記述実験および検討を通 じて,Hydra が備えるべき機能,特に記号的離散状態の表現について踏み 込んだ検討を行った.2. 高信頼実装のためには,求解過程において離散的に切り替わる方程式系の 区間演算技術が必須となる.区間演算においては,離散変化条件の成否が 一般に非決定的となるため,成否が決定的になるような小区間への分割を 行いつつ区間演算を進めるアルゴリズムを提案し,その有効性を確認した.3. ハイブリッドシステムにおける重要かつ厄介な性質として,有限時間内に 無限回の離散的状態変化を起こす Zeno 挙動がある.そこで,与えられた システムがZeno 挙動をもつかどうかの自動検証手法を開発した.Zeno 挙 動に関する推論は数値計算では困難であり,数式処理と限定記号除去によ る解析方式を提案してその有効性を確認した.4. ハイブリッドシステムの検証に伝統的に使われてきたハイブリッドオート マトンとハイブリッド制約モデリング言語との関係づけのために、ハイブ リッド制約プログラムからハイブリッドオートマトンへの自動変換技法を 開発して実装した.5. 既存の制約ソルバ,区間演算,多倍長演算ライブラリを高信頼実装の部品 として活用するための調査・実験・準備を行った.区間演算を用いた常微 分方程式ソルバVNODE-LPに多倍長演算を組込み,求解精度向上における有 効性を多数の例題で調査するとともに,非線形制約求解系Elisaを用いた幾 何モデリングにおける制約不足の問題に対処するためのパターン分割手法 を提案・実験した.

  • リンクつき階層多重集合に基づく統合プログラミング言語モデルLMNtal

    2004年   加藤 紀夫

     概要を見る

    本研究では、統合言語モデルLMNtal実用化の基盤を固めるために下記の研究を遂行して多様な成果を得た。1. プラットフォーム処理系の整備と拡充研究開発のプラットフォームとなるLMNtal逐次処理系をJavaで実装、公開し、バージョンアップを重ねてきた。分散処理系への拡張を念頭に置いて、膜ごとの計算を非同期に実行するための排他制御や協調動作の方式設計および実装を行った。また可視化機能や他言語インタフェース機能の拡充、プロセス文脈機能の強化、生成コードの改善などの各種改良も行った。処理系の規模はおよそ2万行におよぶ。2. 言語設計の洗練LMNtalが分散計算を的確にモデル化する言語モデルとなるように、従来の操作的意味論の一部を見直した。コネクタ(二つのグラフ構造を接続するための言語要素)に関して、どのような操作を構造合同(可逆)と見なし、どのような操作を遷移関係(非可逆)と見なすべきかを考察し、従来の言語仕様の問題点を発見し修正した。3. LMNtalプログラムに対する型体系の設計LMNtalプログラムが形成するプロセス構造を扱うための型体系を設計し、型安全性の証明を行った。この型体系は、膜に出現する可能性のあるアトム(グラフのノード)の種類やリンクのつながり方を定式化するものである。本研究を通じて、実用的な解析のためには、膜に名前を付けて膜の静的な役割を識別することが有効であるとの知見を得た。4. 分散処理系および小規模制御系向け処理系膜に実行位置情報を付加する機能を導入し、通信・キャッシュ・ロック・終了処理等の機構を逐次処理系に付加することにより、LMNtal分散処理系の試作を行った。また、組込み応用に向けて、センサやアクチュエータをLMNtalのアトムとの対応づける方式を考案し、ロボットコントローラ実機上で動作するLMNtalサブセットの実行系を構築して自律移動ロボットの制御を実現した。

  • 並行論理プログラミングに基づく広域分散計算パラダイムの構築

    1998年  

     概要を見る

    並行論理プログラミング言語は、論理プログラミングパラダイムに情報の流れを制御するための同期機構を導入し、並行処理記述のための言語としたものである。なかでも研究提案者の提案した並行論理プログラミング言語GHC(Guarded Horn Clauses)は、簡潔な通信・同期機構をもちながら、構成が動的に変化する並行プロセス系を自然に記述できる柔軟性も併せもつ。 これまでの並行論理プログラミングの研究開発は、主として並列計算機上での高速実行を目標としてきた。一方、コンピュータネットワークの急速な普及と共に、広域分散計算環境で稼働する効率的で安全な分散型アプリケーションを容易に構築するための方法論の確立が急務となっている。そこで本研究では、並行論理プログラミングに基づく広域分散計算パラダイムの確立を目標として、下記の検討を行なった。 宣言型言語とそのプログラミングのもつ簡明さをできるだけ保ちつつ、広域分散計算の記述と非均質計算環境下での実行を可能にする方法の検討。 広域分散環境で稼働する言語処理系に求められる静的プログラム解析技術の確立、およびプログラム解析技術に基づく安全な広域分散ソフトウェア構築方法論の検討。 特に本研究では、広域分散実装のための静的解析技法の確立に重点を置き、並行論理プログラムの参照数解析の体系の提案と理論的整備を行なった。参照数解析とは、複数の参照ポインタをもちうるデータ構造と、単一の参照ポインタしかもたないデータ構造とを、静的プログラム解析によって区別するものである。単一参照のデータ構造に対してはコンパイル時ゴミ集め、記憶域の局所的再利用(local reuse)、データ送信のメッセージパッシングへのコンパイルなどが可能となり、広域分散実装が大幅に単純化、効率化される。本研究ではこの参照数解析の理論的枠組を提案し、解析の安全性を証明した。またこれを、KL1言語用静的解析系klint第2版の機能の一つとして実装し、有効性を確認した。 記号処理言語は動的データ構造の柔軟な作成管理を特徴とするが、分散計算環境における実装は困難とされてきた。これに対して本研究では、記号処理プログラムからも十分な静的解析情報が得られることを示すことができた。簡潔な並行言語を拡張して広域分散計算に適用することによって、単純で検証の容易な広域分散処理記述言語を得ることが期待される。

  • 見込み計算によるインタラクティブ・ソフトウェアの応答性改善法

    1996年  

     概要を見る

     計算機の会話的利用の機会と重要性は最近ますます高まりつつあり、マルチメディア化も大きく進展している。しかし、ほとんどのインタラクティブ・ソフトウェアは、基本的に従来の決定的逐次プログラミング・パラダイムの下に記述されており、計算機性能の著しい向上にもかかわらず、利用者入力に対する応答性能が十分確保されていないことが多い。 そこで本研究では、見込み計算(speculative computation)技法を中心に、利用者タスクとシステムタスクとの並行・並列処理、漸増的計算、実時間処理などの手法を援用することによって、インタラクティブ・ソフトウェアの応答性能を抜本的に改善する方法について検討を進めた。 ネットワークニュースリーダを題材とした実験の結果、利用者の挙動を適切に予測して、コマンド入力後に必要となる処理を可能な限り見込み計算しておくことにより、応答性が大幅に改善できることが実証できた。見込み計算は、フロントエンドのニュースリーダとバックエンドのキャッシュシステムの双方で、各利用者および利用者集団全体の記事購読特性に基づいて行なっている。 さらに本研究では、ニュースリーダでの良好な結果を、WWW記事のキャッシュシステムに適用することを試みた。 WWWにおいては、応答性改善及びネットワーク負荷の抑制を目的として、キャッシュ機能を付加したプロキシサーバが使用されている。しかし、このキャッシュ機能は一度アクセスしたデータを再利用するだけのパッシブなものであり、新たなアクセスには応答性改善効果がない。また、どのデータがキャッシュされているかわからないので、キャッシュの恩恵は偶発的でヒット率の低いものとなる。 そこで、プロキシサーバのキャッシュデータを各利用者毎に整理し、Webブラウザを通して視覚化した。また、キャッシュデータの最新性をバックグラウンドで確認してその更新状況を表示するとともに、今後読む可能性が高いと予測されるデータをトラフィックの少ない時間帯にプリフェッチし、その状況もあわせて視覚化した。一般に、WWW利用時の行動はニュース利用時の行動と比較して予測が困難であるが、見込み計算と視覚化機能との併用によって、良好な応答性能を確保できる見通しを得た。

  • 並行論理プログラミング言語による高速定型処理

    1995年  

     概要を見る

    並行論理プログラミング言語は,論理プログラミング・パラダイムに情報の流れを制御するための同期機構を導入し,並行処理記述のための言語としたものであり,柔軟性と簡潔性を大きな特徴とする。しかしながら,これまで,非定型的な並列記号処理のための言語と位置づけられてきたために,定型処理の記述性と効率が不十分であった。一方,並列記号処理の本格的応用のなかには,柔軟な記号処理と,数値計算のような高速定型処理の双方を要するものが増加しつつある。そこで本研究では,並行論理プログラミング言語における効率的な配列操作の枠組の確立を目標として,その基礎研究を行なった。 ベースとなる言語として,静的モード体系を持つ言語Moded Flar GHCを採用した。静的モード体系は,並行論理プログラムの性質に関するもっとも基礎的な情報を提供するもので,制約充足問題として定式化することができ,グラフ単一化によって効率良く解析することができる。また,同様の制約ベースの技法によって,データ型,および参照数(データを指すポインタの数)の解析も可能であることを明らかにした。参照数の解析は,単一代入言語における配列の破壊的操作にとって本質的である。 以上の解析情報は特定の実装に依存しない基礎的情報であるが,浮動小数点演算や配列を用いた処理を最適化し,手続き型言語における効率に近づけるには,さらに,データの具体化状態に関する解析も必要であり,その方式も検討した。 これらの解析情報に基づき,並行処理プログラミング言語処理系KLIC上の浮動小数点数処理および配列処理の高速化を試みた。KLICは,高い基本性能を実現するとともに,ジェネリックオブジェクト機構によってデータ型などの拡張性を確保し,それによって浮動小数点や配列を実装している。しかしながら,ジェネリックオブジェクトによる実装は,空間的,時間的なオーバーヘッドが大きい。 本研究では,上記の各種解析情報によって,ジェネリックオブジェクトによる実装のオーバーヘッドを除去する方法を検討し,実験を行なった。これまでに,典型的な浮動小数点演算で13倍以上,配列の更新演算については,破壊的更新が可能なことが参照数解析によってわかる場合,3.5倍以上の性能向上が得られた。配列演算は,添字検査の手間の比率が大きいため,詳細なプログラム解析によってさらなる性能向上が可能である。今後も,これらの検討を進めることにより,非手続き型言語における配列操作パラダイムの確立を目指し,それを通じて並行論理プログラミングの応用分野の拡大を図ってゆく予定である。

▼全件表示

海外研究活動

  • 並行制約プログラミングに基づく広域分散計算パラダイムの構築

    2000年09月
    -
    2001年02月

    シンガポール   シンガポール国立大学

 

現在担当している科目

▼全件表示

 

委員歴

  • 2013年04月
    -
    2017年12月

    New Generation Computing (Ohmsha and Springer)  Associate Editor-In-Chief

  • 2011年
    -
    2014年

    Asian Association for Foundations of Software (AAFS)  Co-Chair

  • 2001年11月
    -
    2013年03月

    New Generation Computing (Ohmsha and Springer)  Area Editor (Programming and Architecture分野)

  • 2010年
    -
     

    Eighth Asian Symposium on Programming Languages and Systems (APLAS 2010, Shanghai, China, November-December 2010)  プログラム委員長

  • 2004年04月
    -
    2008年03月

    コンピュータソフトウェア(日本ソフトウェア科学会機関誌)  編集委員長

  • 2001年01月
    -
    2004年12月

    Theory and Practice of Logic Programming (Cambridge University Press)  Area Editor (Design and Analysis of Languages and Systems分野)

  • 2000年04月
    -
    2002年03月

    人工知能学会  理事

  • 2001年
    -
     

    Fifth International Symposium on Functional and Logic Programming (FLOPS 2001, Tokyo, March 7-9, 2001)  プログラム委員長 (Herbert Kuchen 氏と共同)

  • 1998年04月
    -
    2000年03月

    情報処理学会論文誌:プログラミング  編集委員長

  • 1992年10月
    -
    1999年11月

    Journal of Logic Programming (North-Holland)  Area Editor (Design and Analysis of Languages and Systems分野)

  • 1997年
    -
     

    並列処理シンポジウム'97 (神戸)  プログラム委員長

  • 1997年
    -
     

    Asian Computing Science Conference (ASIAN'97、Kathmandu, Nepal, December 9-12, 1997)  プログラム委員長 (R.K. Shyamasunder氏と共同)

  • 1991年
    -
     

    International Logic Programming Symposium (ILPS'91, San Diego, U.S.A.)  プログラム委員長 (Vijay Saraswat 氏と共同)

  • 2001年04月
    -
    2007年03月

    日本ソフトウェア科学会  理事

  • 1998年04月
    -
    2000年03月

    情報処理学会  プログラミング研究会 主査

▼全件表示