Details of a Researcher - UEDA, Kazunori

写真a

UEDA, Kazunori

Scopus Paper Info

Paper Count: 82 Citation Count: 460 h-index: 12

Click to view the Scopus page. The data was downloaded from Scopus API in April 23, 2024, via http://api.elsevier.com and http://www.scopus.com .

Google Scholar Information (Citations per year)

Citation Count: 2657 h-index: 24 i10-index: 50

Click to view the Google Scholar page.

Scopus Information

Affiliation

Faculty of Science and Engineering, School of Fundamental Science and Engineering

Job title

Professor

Degree

工学博士 ( 1986 東京大学 )
Doctor of Engineering

Homepage URL

http://www.ueda.info.waseda.ac.jp/~ueda/index-j.html

Research Experience

2010

-

Now

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

-

Now

Waseda University Faculty of Science and Engineering
2006

-

2016

National Institute of Informatics
2011

-

2012

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

-

2007

Waseda University School of Science and Engineering
1997

-

2003

Waseda University School of Science and Engineering
2000

-

2001

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

-

2000

The University of Tokyo Faculty of Science
1993

-

1997

Waseda University School of Science and Engineering
1994

-

1995

Ibaraki University
1983

-

1993

NEC Corporation
1985

-

1992

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

▼display all

Education Background

　

-

1983

University of Tokyo Graduate School, Division of Engineering
　

-

1978

University of Tokyo Faculty of Engineering

Committee Memberships

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

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

▼display all

Professional Memberships

　

　

　

IEEE Computer Society
　

　

　

Association for Computing Machinary
　

　

　

人工知能学会
　

　

　

情報処理学会
　

　

　

日本ソフトウェア科学会

Research Areas

Theory of informatics / Software

Research Interests

logic and constraint programming
Hybrid Systems
Concurrency and Parallelism
Design and Implementation of Programming Languages

Awards

フェロー

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

2015 情報処理学会
基礎研究賞

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

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

2000
第７回日本IBM科学賞

1993
第３回元岡賞

1988
功労賞

2010 日本ソフトウェア科学会
人工知能学会2002年度全国大会ベストプレゼンテーション賞

2003
日本ソフトウェア科学会第１９回高橋奨励賞

2002
情報処理学会第３０回全国大会学術奨励賞

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

1985

▼display all

Papers

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 [Refereed]

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

44th IEEE Annual Computers, Software, and Applications Conference(COMPSAC) 1113 - 1114 2020 [Refereed]

DOI

Scopus

1

Citation

(Scopus)
Declarative Semantics of the Hybrid Constraint Language HydLa.

Kazunori Ueda, Hiroshi Hosobe, Daisuke Ishii

CoRR abs/1910.12272 2019 [Refereed]
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 [Refereed]

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 [Refereed]
Logic/Constraint Programming and Concurrency: The hard-won lessons of the Fifth Generation Computer project.

Kazunori Ueda

Sci. Comput. Program. 164 3 - 17 2018 [Refereed]

Authorship：Lead author

DOI

Scopus

3

Citation

(Scopus)
Implementation of LMNtal Model Checkers: a Metaprogramming Approach.

Yutaro Tsunekawa, Taichi Tomioka, Kazunori Ueda

J. Object Technol. 17 ( 1 ) 1 - 28 2018 [Refereed]

DOI

Scopus

1

Citation

(Scopus)
Name Binding is Easy with Hypergraphs.

Alimujiang Yasen, Kazunori Ueda

IEICE Trans. Inf. Syst. 101-D ( 4 ) 1126 - 1140 2018 [Refereed]

DOI

Scopus

1

Citation

(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 [Refereed]

DOI

Scopus

2

Citation

(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 [Refereed]

DOI

Scopus

1

Citation

(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 [Refereed]

DOI

Scopus

1

Citation

(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 [Refereed]

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 [Refereed]
Optimized Canonical Labeling Algorithm for Graph Rewriting Systems

MIYAHARA Kazuhiro, UEDA Kazunori

Computer Software 33 ( 1 ) 1_126 - 1_149 2016

　View Summary

In graph-based model checking, systems are modeled with graph structures which are highly expressive and feature a symmetry reduction mechanism. However, it involves frequent isomorphism checking of graphs generated in the course of model checking. Canonical labeling of graphs, which gives a unique representation to isomorphic graphs, is expected to be an effective method to check isomorphism among many graphs efficiently. It is therefore important to efficiently compute canonical forms of graphs in graph rewriting systems. For this purpose, we propose an optimization technique for McKay's canonical labeling algorithm that reuses information of graph structures that does not change by rewriting. To enable reuse, we reformulated McKay's algorithm to clarify what substructures of graphs are utilized in its execution, and designed an algorithm for successive graph canonicalization that organizes graph information in such a way that recomputation may be minimized. We evaluated the performance of the proposed algorithm, and found that it achieved sublinear time complexity with respect to the number of vertices for many cases of re-canonicalization.

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

宮原和大, 上田和紀

コンピュータソフトウェア 33 ( 1 ) 126 - 149 2016.01 [Refereed]
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

Citation

(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 [Refereed]

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 [Refereed]

DOI

Scopus

3

Citation

(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 [Refereed]

DOI
Validated Interval Computation of Reachable Sets of Nonlinear Hybrid Systems

ISHII Daisuke, UEDA Kazunori

Journal of The Society of Instrument and Control Engineers 53 ( 12 ) 1086 - 1092 2014.12 [Refereed]

DOI CiNii
Towards a Substrate Framework of Computation

Kazunori Ueda

Concurrent Objects and Beyond, Lecture Notes in Computer Science 8665 341 - 366 2014 [Refereed] [Invited]

Authorship：Lead author

DOI

Scopus

2

Citation

(Scopus)
Reduction of the Number of States and the Acceleration of LMNtal Parallel Model Checking

Ryo YASUDA, Taketo YOSHIDA, Kazunori UEDA

Transactions of the Japanese Society for Artificial Intelligence 29 ( 1 ) 182 - 187 2014.01 [Refereed]

　View Summary

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 [Refereed]
ハイブリッド制約言語プログラムのハイブリッドオートマトンへの変換アルゴリズム

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

日本ソフトウェア科学会第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 [Refereed]
HyperLMNtal: An Extension of a Hierarchical Graph Rewriting Model

Kazunori Ueda, Seiji Ogawa

KI - Künstliche Intelligenz 26 ( 1 ) 27 - 36 2012.02 [Refereed]

DOI

Scopus

9

Citation

(Scopus)
LMNtal実行時処理系の並列モデル検査器への発展

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

コンピュータソフトウェア 28 ( 4 ) 137 - 157 2011.11 [Refereed]
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 [Refereed]
ハイブリッドシステムモデリング言語HydLaの実装

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

日本ソフトウェア科学会第28回大会論文集 ( 6.00E-04 ) 1 - 11 2011.09
An Execution Algorithm for the Hybrid System Modeling Language HydLa

28 ( 3 ) 167 - 172 2011.07 [Refereed]
ハイブリッドシステムモデリング言語HydLaの数式処理実行系

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

情報処理学会第73回全国大会講演論文集 247 - 248 2011.03
Speedup of OWCTY Model Checking Algorithm Using Strongly Connected Components

Toshiki KAWABATA, Fumiyoshi KOBAYASHI, Kazunori UEDA

Transactions of the Japanese Society for Artificial Intelligence 26 ( 2 ) 341 - 346 2011 [Refereed]

　View Summary

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の宣言的意味論(レター論文)

Kazunori Ueda, Hiroshi Hosobe, Daisuke Ishii

Computer Software 28 ( 1 ) 306 - 311 2011.01 [Refereed]

Authorship：Lead author

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

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

コンピュータソフトウェア 27 ( 4 ) 197 - 214 2010.11 [Refereed]
ハイブリッド制約言語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

Kazunori Ueda

Theoretical Computer Science 410 ( 46 ) 4784 - 4800 2009.11 [Refereed]

Authorship：Lead author

DOI CiNii

Scopus

16

Citation

(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 [Refereed]
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 [Refereed]
制約階層によるハイブリッドシステムのモデリング手法

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

日本ソフトウェア科学会第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 [Refereed]
c-sat: A Parallel SAT Solver for Clusters

Kei Ohmura, Kazunori Ueda

Theory and Applications of Satisfiability Testing - SAT 2009, Lecture Notes in Computer Science 5584 524 - 537 2009 [Refereed]

DOI CiNii

Scopus

31

Citation

(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 [Refereed]

DOI

Scopus

7

Citation

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

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

電子情報通信学会コンカレント工学研究会(CST), 信学技報 108 ( 415 ) 67 - 70 2009.01
制約概念に基づくハイブリッドシステムモデリング言語HydLa

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

第5回システム検証の科学技術シンポジウム(SSV2008)予稿集 1 - 6 2008.11
ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法

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

情報処理学会論文誌：数理モデル化と応用 1 ( 1 ) 149 - 159 2008.09 [Refereed]
区間演算を用いたODE Solverにおける任意精度演算の導入とパラメタ最適化

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

情報科学技術フォーラム講演論文集 7 ( 1 ) 75 - 78 2008.08
論理・制約プログラミングと並行計算

上田和紀

コンピュータソフトウェア 25 ( 3 ) 49 - 54 2008.08 [Refereed]

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

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

第6回ディペンダブルシステムワークショップ(DSW2008)論文集 101 - 104 2008.07
階層グラフ書換え言語LMNtalの処理系

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

コンピュータソフトウェア 25 ( 2 ) 47 - 77 2008.05 [Refereed]
Encoding Distributed Process Calculi into LMNtal

Kazunori Ueda

Electronic Notes in Theoretical Computer Science 209 187 - 200 2008.04 [Refereed]

Authorship：Lead author

DOI

Scopus

9

Citation

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

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

情報処理学会研究報告：数理モデル化と問題解決(MPS) 68 133 - 136 2008.03
数式処理・quantifier eliminationを用いたハイブリッドシステムのZeno状態の導出手法

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

人工知能学会全国大会論文集 1D1-3 2008
階層グラフ書換えモデルに基づく統合プログラミング言語LMNtal

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

コンピュータソフトウェア 25 ( 1 ) 124 - 150 2008.01 [Refereed]

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

　View Summary

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 [Refereed]
階層グラフ可視化ツール"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 [Invited]
後継関数を持つリスト型非線形再帰プログラムに対する再帰除去法

市川祐輔, 上田和紀

情報科学技術レターズ 6 9 - 12 2006.09 [Refereed]
分散プロセス計算の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 [Refereed]
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 [Invited]
Logic Programming and Concurrency: a Personal Perspective

Kazunori Ueda

The ALP NewsLetter 19 ( 2 ) 2006.05 [Invited]
アセンブリプログラムの構造を利用したキャッシュヒント自動付加

稲垣良一, 上田和紀

先進的計算基盤システムシンポジウム (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 [Refereed]
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 [Refereed]
階層グラフ書換え言語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 [Invited]
確率モデル遺伝的アルゴリズム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
The Language Model LMNtal

UEDA Kazunori, KATO Norio, 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

DOI CiNii

Scopus

1

Citation

(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 [Refereed]

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 [Refereed] [Invited]

　View Summary

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 [Refereed]

Authorship：Lead author
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 [Invited]
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

　View Summary

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

K Ueda

COMPUTATIONAL LOGIC: LOGIC PROGRAMMING AND BEYOND, PT I 2407 138 - 161 2002 [Refereed] [Invited]

　View Summary

This paper discusses the construction of a meta-interpreter, of Flat GHC, one of the simplest and earliest concurrent constraint languages.
Meta-interpretation has a long history in logic programming, and has been applied extensively to building programming systems, adding functionalities, modifying operational semantics and evaluation strategies, and so on. Our objective, in contrast, is to design the pair of (i) a representation of programs suitable for code mobility and (ii) a pure interpreter (or virtual machine) of the represented code, bearing networked applications of concurrent constraint programming in mind. This is more challenging than it might seem; indeed, meta-interpreters of many programming languages achieved their objectives by adding small primitives into the languages and exploiting their functionalities. A meta-interpreter in a pure, simple concurrent language is useful because it is fully amenable to theoretical support including partial evaluation. After a number of trials and errors, we have arrived at treecode, a ground-term representation of Flat GHC programs that can be easily interpreted,, transmitted over the network, and converted back to the original syntax. The paper describes how the interpreter works, where the subtleties lie,, and what its design implies. It also describes how the interpreter, given the treecode of a program, is partially evaluated to the original program by the unfold/fold transformation system for Flat GHC.
Kima: An automated error correction system for concurrent logic programs

Yasuhiro Ajiro, Kazunori Ueda

Automated Software Engineering 9 ( 1 ) 67 - 94 2002.01 [Refereed]

　View Summary

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

Citation

(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 [Refereed]

　View Summary

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 [Refereed] [Invited]
日本ソフトウェア科学会第18回大会講演論文集

日本ソフトウェア科学会 2001.09
計算連続体に基づくソフトウェア実現法の提案

日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会 2001.09 [Refereed]
インタフェースに基づく並行論理プログラム最適化コンパイラの構成法

日本ソフトウェア科学会第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 [Refereed]
並行論理プログラムにおける逐次実行部分の抽出方法論

第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 [Invited]
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 [Refereed]
並行論理プログラムのプログラム空間に関する考察

2000年度人工知能学会全国大会(第14回)論文集 pp.449-452 2000.07
Linearity Analysis of Concurrent Logic Programs

K Ueda

Proc. International Workshop on Parallel and Distributed Computing for Symbolic and Irregular Applications, Ito, T. and Yuasa, T. (eds.), World Scientific pp.253-270 253 - 270 2000.05

　View Summary

Automatic memory management and the hiding of the notion of pointers are the prominent features of symbolic processing languages. They make programming easy and guarantee the safety of memory references. For the memory management of linked data structures, copying garbage collection is most widely used because of its simplicity and desirable properties. However, if certain properties about runtime storage allocation and the behavior of pointers can be obtaind by static analysis, a compiler may be able to generate object code closer to that of procedural programs. In the fields of parallel, distributed and real-time computation, it is highly desirable to be able to identify data structures in a program that can be managed without using garbage collection. To this end, this paper proposes a framework of linearity analysis for a concurrent logic language Moded Flat GHC, and proves its basic property. The purpose of linearity analysis is to distinguish between fragments of data structures that may be referenced by two or more pointers and those that cannot be referenced by two or more pointers. Data structures with only one reader are amenable to compile-time garbage collection or local reuse. The proposed framework of linearity analysis is constraint-based and involves both equality and implicational constraints. It has been implemented as part of klint v2, a static analyzer for KL1 programs.
第五世代核言語ができるまで

第3回システムおよびプログラミングの応用に関するワークショップ (SPA2000) 2000.03 [Invited]
共有オブジェクト空間を用いた分散プログラミング支援ミドルウェア 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 [Refereed]
Kima - an Automated Error Correction System for Concurrent Logic Programs.

Yasuhiro Ajiro, Kazunori Ueda

Computer Software 18 ( 0 ) 122 - 137 2000 [Refereed]

DOI

Scopus

1

Citation

(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 [Refereed]

Authorship：Lead author
全文検索システム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 [Refereed] [Invited]
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 [Refereed]
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

Authorship：Lead author
全文検索システム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

Authorship：Lead author
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 [Refereed]

　View Summary

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 [Refereed]
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

Authorship：Lead author

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 [Refereed]
制約に基づく解析による並行論理プログラムの自動デバッグ

人工知能学会全国大会論文集 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 [Refereed]
並列計算機システムFOLON上へのPVMの移植と評価

情報処理学会研究報告/情報処理学会 96;80 (96-ARC-119) 1996.08
並行論理プログラムのモード解析手法を用いた静的診断

人工知能学会全国大会論文集/人工知能学会 1996.06
モード誤りをもつ並行論理プログラムの静的デバッグ手法

1996年並列処理シンポジウム論文集/情報処理学会 1996.06 [Refereed]
Experiences with Strong Moding in Concurrent Logic/Constraint Programming

K Ueda

Proc. International Workshop on Parallel Symbolic Languages and Systems (T. Ito, R. H. Halstead, C. Queinnec (Eds.)), Lecture Notes in Computer Science 1068/Springer-Verlag 1068 134 - 153 1996.04

　View Summary

Strong moding is turning out to play fundamental roles in concurrent logic programming (or in general, concurrent constraint programming) as strong typing does but in different respects. ''Principal modes'' can most naturally be represented as feature graphs and can be formed by unification. We built a mode analyzer, implementing mode graphs and their operations by means of concurrent processes and streams (rather than records and pointers). This is a non-trivial programming experience crith complicated process structures and has provided us with several insights into the relationship between programming with dynamic data structures and programming with dynamic process structures. The mode analyzer was then applied to the analyzer itself to study the characteristics of the mode constraints it imposed and of the form of large mode graphs. Finally, we show how our framework based on principal moding can be extended to deal with (1) random-access data structures, (2) mode polymorphism (3) higher-order constructs, and (4) various non-Herbrand constraint systems.
並列計算機システム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 [Invited]
I/O Mode Analysis in Concurrent Logic Programming

Kazunori Ueda

Theory and Practice of Parallel Programming (Ito, T. and Yonezawa, A., eds.), Lecture Notes in Computer Science 907/Springer-Verlag 907 356 - 368 1995.05

　View Summary

This paper briefly reviews concurrent logic programming and the I/O mode system designed for the concurrent logic language Flat GHC. The mode system plays fundamental roles both in programming and implementation in almost the same way as type systems do but in different respects. It provides us with the information on how data are generated and consumed and thus the view of “data as resources”. It statically detects bugs resulting from ill-formed dataflow and advocates the “programming as wiring” paradigm. Well-modedness guarantees the safety of unification, the basic operation in concurrent logic programming. Information on the numbers of access paths to data can be obtained by slightly extending the framework, which can be used for compile-time garbage collection and the destructive update of structures.

DOI

Scopus

4

Citation

(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 [Refereed]

Authorship：Lead author

　View Summary

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 [Refereed] [Invited]
Moded Flat GHC for Data-Parallel Programming

Proc. FGCS'94 Workshop on Parallel Logic Programming, ICOT, Tokyo 27-35 1994 [Refereed]

Authorship：Lead author
Message-Oriented Parallel Implementation of Moded Flat GHC

K. Ueda, M. Morita

New Generation Computing 11 ( 3-4 ) 323 - 341 1993 [Refereed]

Authorship：Lead author

　View Summary

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 [Refereed] [Invited]
第五世代コンピュータ技術の開花と結実に向けて

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 [Refereed]

Authorship：Lead author
並列論理型言語上の制約充足方式の比較

YOKOO MAKOTO, UEDA KAZUNORI

情報処理学会論文誌 32 ( 3 ) 296 - 303 1991 [Refereed]

CiNii
Design of the Kernel Language for the Parallel Inference Machine

K. Ueda, T. Chikayama

Computer Journal 33 ( 6 ) 494 - 500 1990.12 [Refereed]

　View Summary

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 [Invited]
A New Implementation Technique for Flat GHC

K. Ueda, M. Morita

Logic Programming: Proceedings of the Seventh International Conference 3 - 17 1990 [Refereed]

Authorship：Lead author
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 [Refereed] [Invited]

Authorship：Lead author
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 [Refereed] [Invited]
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 [Invited]
Transformation Rules for GHC Programs

Kazunori Ueda, Koichi Furukawa

Proc. Int. Conf. on Fifth Generation Computer Systems 1988, ICOT, Tokyo 582-591 1988 [Refereed]
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 [Refereed]
Making Exhaustive Search Programs Deterministic, Part II

Kazunori Ueda

Proc. Fourth Int. Conf. on Logic Programming, The MIT Press, Cambridge, Mass. 356-375 1987 [Refereed]
並列プログラミング

情報処理 27 ( 9 ) 995 - 1004 1986.09 [Invited] [Domestic journal]

Authorship：Lead author, Corresponding author
Introduction to Guarded Horn Clauses

Kazunori Ueda

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 [Refereed]

　View Summary

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

54

Citation

(Scopus)
Guarded Horn Clauses and Experiences with Parallel Logic Programming

Tanaka, Jiro, Ueda, Kazunori, Miyazaki, Toshihiko, Takeuchi, Akikazu, Matsumoto, Yuji, Furukawa, Koichi

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 [Refereed]

Authorship：Lead author

DOI

Scopus

7

Citation

(Scopus)
Concurrent Prolog Compiler on Top of Prolog

Proc. 1985 Symp. on Logic Programming, IEEE Computger Society 119-126 1985 [Refereed]
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 [Refereed]

　View Summary

Mandala is a programming system aimed for developing knowledge information processing systems in logic programming framework. It is not only a knowledge programming system but also a basis for a knowledge base management system. The nature of this duality comes directly from two-facedness of logic programming, that is, both procedural and declarative interpretation. Mandala provides users with parallel execution environment, allowing them to describe multiple-processes. On this parallel execution environment, cooperative problem solving systems can be constructed, in which more than one problem solver can be active in parallel. Mandala realizes object oriented programming using a process mechanism in KL1, thus manipulating dynamically changing states. Objects in Mandala can be seen as problem solvers which have inference engines and knowledge base.
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 [Refereed]
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 [Refereed]
述語論理型言語における副作用によらない入出力と文字列操作

NAKASHIMA HIDEYUKI, UEDA KAZUNORI, TOMURA SATORU

情報処理学会論文誌 24 ( 6 ) 745 - 753 1983 [Refereed]

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

計測自動制御学会論文集 5/4,486-491 1979 [Refereed]

▼display all

Books and Other Publications

AI事典第3版

( Part： Contributor, 1.2「第五世代コンピュータ」(pp.4-5))

近代科学社 2019.12
人工知能学大事典

( Part： Contributor, 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

Lecture Notes in Computer Science 2024, Springer-Verlag 2001
Advances in Computing Science: ASIAN '97

Lecture Notes in Computer Science 1345, Springer-Verlag 1997
並列処理シンポジウムJSPP'97論文集

情報処理学会 1997
楽しいプログラミング：記号の世界

中島秀之, 上田和紀

岩波書店 1992
Logic Programming : Proceedings of the 1991 International Symposium

The MIT Press 1991
続・新しいプログラミング・パラダイム

井田哲雄, 田中二郎編, 上田和紀他共著( Part： Joint author, 第1章 "並行プログラミングとGHC" (pp.1-34))

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

( Part： Contributor, 2.1.4(1) 「Concurrencyと並列性」)

産業調査会事典出版センター 1989.08
並列論理型言語GHCとその応用

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

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

上田和紀( Part： Joint author, pp.87-128)

bit 臨時増刊，共立出版 1981.10

▼display all

Works

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

Software

2010

-

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

Software

2002

-

Now

Presentations

言語をつくる

[Invited]

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

Presentation date： 2018.08
Logic/Constraint Programming and Concurrency: The Hard-Won Lessons of the Fifth Generation Computer Project

[Invited]

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

Presentation date： 2016.03
Hierarchical graph rewriting as a unifying model and language of concurrency

[Invited]

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

Presentation date： 2006.11
LMNtal: a unifying declarative language

[Invited]

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

Presentation date： 2006.07
Constraint-Based Concurrency and Beyond

[Invited]

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

Presentation date： 2005
LMNtal: a language model with links and membranes

[Invited]

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

Presentation date： 2004.06
Resource-Passing Concurrent Programming (advanced tutorial)

[Invited]

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

Presentation date： 2001.11
Resource-Passing Concurrent Programming

[Invited]

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

Presentation date： 2001.10
Strong Moding in Concurrent Logic/Constraint Programming (advanced tutorial)

[Invited]

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

Presentation date： 1995.06
Designing a Concurrent Programming Language

[Invited]

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

Presentation date： 1990.10
Paralleism in Logic Programming

[Invited]

IFIP 11th World Computer Congress

Presentation date： 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 [Invited]

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

Presentation date： 1988.11
Concurrent Logic Programming Languages (tutorial)

[Invited]

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

Presentation date： 1987
Guarded Horn Clauses

[Invited]

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

Presentation date： 1986.12
Teaching (Constraint) Logic Programming

G. Gupta, M.V. Hermenegildo, U. Nillson, P. Stuckey, K. Ueda [Invited]

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

Presentation date： 2003.12
The Future of Logic Programming (panel)

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

Presentation date： 1991.11

▼display all

Research Projects

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

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

Project Year :

2018.06

-

2021.03

　View Summary

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

科学研究費基盤研究（Ｂ）

Project Year :

2018.04

-

2021.03

　View Summary

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

Project Year :

2015.04

-

2018.03

　View Summary

Towards the foundations for computing and programming of cyber-physical systems, we studied language constructs and semantics of general-purpose high-level programming languages that allow us to represent and handle continuous quantities and the notion of time. Our working hypothesis was that those languages should be concurrent programming languages featuring concurrency and communication and, at the same time, be constraint programming languages featuring continuous quantities and uncertainties. Through detailed study of existing languages, we clarified many of theoretical foundations and necessary language constructs, including (i) constraint hierarchies and its semantics, (ii) the notion of time, (iii) data domain, and (iv) description of dynamically evolving concurrent systems
Deepening the implemenation technology of high-level modeling language implementations integrated with verifiers

Project Year :

2014.04

-

2017.03

　View Summary

The goal of this research was to deepen the implementation technology of high-level modeling languages that support highly abstract and general data representation such as real numbers and graph structures. To achieve reliable simulation of hybrid systems that make both continuous and discrete changes, we developed various techniques including a method for integrating numerical computation with guaranteed accuracy and symbolic computation, and greatly improved the solution capability and performance of the symbolic simulator of the constraint-based modeling language HydLa. For the runtime system of the graph-rewriting modeling language LMNtal, a number of new techniques were developed, e.g., for expressive hypergraph rewriting and efficient parallel model checking, and the system was evolved into a more powerful verification tool. The developed implementations were made publicly available as open-source software
Evolutionary development of a model checker compiler using verification technology and non-standard type systems

Project Year :

2012.04

-

2015.03

　View Summary

Modeling and verification of various systems are expected to be important applications of non-procedural high-level languages. The Principal Investigator has long worked on the design and implementation of a modeling language based on graph rewriting that supports ordinary execution and model checking in a unified framework, but the evolution and verification of its compiler has been recognized as a challenging issue. In this study, we formalized and verified graph rewriting operations performed by the abstract machine that is the interface between the compiler and the runtime, and made a step towards the verification of a graph rewriting compiler. Also, we established novel type systems for the graph rewriting language that will help the analysis, understanding and compiler optimization of models. One of them handles microscopic connectivity of graphs and hypergraphs, while the other handles the global shape of graphs
Implementations of high-level modeling languages that integrate high-performance verifiers

Project Year :

2011.04

-

2014.03

　View Summary

Modeling and verification technologies of natural, symbolic and cyber-physical systems are becoming increasingly important. The aim of this research was to demonstrate the viability of high-level modeling languages based on mathematical notions such as graphs, sets, equations and inequations whose generality goes far beyond Computer Science. To achieve this goal, we constructed two publicly available language implementations that integrate runtime systems and verifiers. One of them is an implementation of the graph rewriting language LMNtal, which has now evolved into a parallel model checker with hypergraph rewriting capabilities; the other is an implementation of the hybrid constraint language HydLa, which has evolved into a non-deterministic symbolic execution system for hybrid systems with uncertainties
Study of SAT-based constraint optimization problem solving and its parallel distributed processing

Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research

Project Year :

2008

-

2012

TAMURA Naoyuki, BANBARA Mutsunori, HIRAYAMA Katsutoshi, INOUE Katsumi, IWANUMA Koji, NABESHIMA Hidetomo, YAMAMOTO Yoshitaka, YOKOO Makoto, HASEGAWA Ryuzo, FUJITA Hiroshi, KISHIMURA Miyuki, UEDA Kazunori

　View Summary

We conducted the research on SAT technologies for Constraint Satisfaction and Optimization Problems and their parallel/distributed implementations, and published 105 refereed papers and made 67 presentations. In addition, world's leading softwares were developed including a SAT-based CSP/COP solver Sugar which won at the 2008 and 2009 CSP Solver Competitions in global constraint categories, a CDCL type SAT solver GlueMiniSat which won at the 2011 SAT Competition in Applications UNSAT category, and a partial Max-SAT solver QMaxSAT which won at the 2010 and 2011 Max-SAT evaluation in Application category
High-level hybrid constraint modeling language and its reliable implementation

Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research

Project Year :

2008

-

2011

UEDA Kazunori, ISHII Daisuke, HOSOBE Hiroshi

　View Summary

We have designed a high-level modeling language HydLa for the reliable simulation and verification of hybrid systems that involve both continuous and discrete changes, and established its declarative semantics and an execution algorithm. Features of HydLa include (i) declarative description employing well-established mathematical and logical notations, (ii) the use of constraints to represent and handle uncertain information, and (iii) constraint hierarchies to allow concise description. We have also established an interval-based solution algorithm of discrete changes to guarantee the correctness of simulation and verification in the existence of uncertain information, and built a prototype integrated implementation equipped with main features of HydLa
Highly Scalable Software Construction Basis for Information Explosion Era

Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research

Project Year :

2006

-

2011

CHIKAYAMA Takashi, YUASA Taiichi, UEDA Kazunori, TAURA Kenjiro, ENDO Toshio, YOKOYAMA Daisaku, UMATANI Seiji

　View Summary

To cope with the explosive increase of data amount, frameworks for flexible description of software for widely distributed highly parallel information systems are required. For this purpose, programming languages, middleware systems, and veri-fication systems for highly complicated software have been investigated, and such systems have been proposed, designed, implemented and evaluated the performance. Represent-ative resultant software systems are made open to public
計算機科学における離散と連続に関する調査と新しい展開

科学研究費基盤研究（Ｃ）

Project Year :

2006

-

2007

　View Summary

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

科学研究費特定領域研究

Project Year :

2006

-

2007

　View Summary

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

Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research

Project Year :

2004

-

2007

UEDA Kazunori, KATO Norio

　View Summary

LMNtal is a language model developed by the grantees to unify various computational models featuring multiset rewriting, concurrency and mobility in a concise setting. The purpose of the project has been to grow LMNtal from a hierarchical graph rewriting model to a practical programming language by designing necessary language constructs, establishing implementation techniques, building a full-fledged LMNtal system, and making it widely available.The main results of the project are as follows :(a) Establishing LMNtal as a programming language-we have studied and designed how to incorporate basic datatypes and operations, a module system, and foreign-language interface into hierarchical graph rewriting, and built a diverse range of libraries using them.(b) Establishing implementation techniques and building a full-fledged system-we have built a compiler from LMNtal into dedicated intermediate code and a runtime system that runs the intermediate code. In particular, we have designed and implemented asynchronous execution scheme that uses multiple tasks, an optimizer for individual tasks, and a translator from intermediate code into Java. We have also designed and implemented a visualizer featuring automatic graph drawing.(c) Verifying the expressive power-in order to see if LMNtal is powerful enough to express fundamental concepts in computation, we have encoded diverse computational models including the pi-calculus, the ambient calculus, the lambda calculus and CHR(Constraint Handling Rules), and ran them on our LMNtal system.The LMNtal system we have developed consists of about 50,000 lines of code, and is available via http://www.ueda.info.waseda.ac.jp/lmtal/
構造的分子計算理論-自律的計算系の解析と設計のための基礎理論

科学研究費特定領域研究

Project Year :

2002

-

2006
Software Development based on Continuous Computing Resources

Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research

Project Year :

2001

-

2006

YUASA Taiichi, CHIKAYAMA Takashi, UEDA Kazunori, MORI Shinichiro, YASUGI Masahiro, KOMIYA Tsuneyasu

　View Summary

In order to make it possible to construct complexity analysis models and software systems that can cope with both extent and locality of computer systems, we have been working to revisit, unify and develop existing computation concepts from various points of view, based on the notion of Continuous Computing Resources. The major outcomes of this project are the following.1. Complexity Analysis based on Continuous Computing Resource: We proposed a computation model that can uniformly and concisely express various concepts of computation from the memory hierarchy of a single computer to network delay among computers. We showed that complexity analysis results based on this model reflect real computation more precisely than previous models. In order to make it easier to understand the behavior of sophisticated parallel algorithms, we designed a virtual machine of the model and implemented language systems including simulators and visualizers.2. Concurrent Language Model LMNtal: We designed LMNTal (pronounced as "elemental"), a scalable language model for concurrent computation based on hierarchical graph reduction. On this model, we have established techniques for process structure analysis and implemented this model as realistic and useful programming languages. Since hierarchical graph reduction includes a variety of computation models such as multi-set rewriting models and self-organizing models, it is expected that our results will be useful as a bridge between existing computation models.3. Language Implementation based on Locality: We showed that runtime efficiency of programming language systems can be remarkably improved by focusing on locality. A typical example is the locality improvement by the use of copying garbage collection based on "hierarchical clustering of data objects". This technique is proposed by further improving the existing technique where live objects are copied in depth-first order, with a small stack area and additionally with a queue that is used in case of stack overflow. This technique improves not only the locality in the virtual memory, but also the locality in the CPU cache, and thus allows high performance implementations on real computer systems
Wide-Area and Distributed Computation Paradigm Based on Concurrent Logic Programming

Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research

Project Year :

1999

-

2002

UEDA Kazunori

　View Summary

Concurrent logic languages provide natural mechanisms for describing concurrent computation by introducing dataflow synchronization on single-assignment variables. Previous work on concurrent logic programming focused on efficient parallel computation. Our research, in contrast, focused on distributed, wide-area computation and studied (1) declarative programming under non-uniform computational environments and (2) static analysis for safe distributed programs. Our results can be summarized as follows :1. Seamless distributed implementation - We designed and implemented network-transparent distributed logical variables (single-assignment channels) to transparently interconnect KL1 programs running on non-uniform computational nodes using sockets. We also designed naming service used for the naming and resolution of distributed logical variables. An exception handling mechanism was also designed and implemented.2. Resource management under distributed environments - We designed and implemented a linear type system for concurrent logic programs that statically analyzes data sharing by logical variables. Furthemore, we proposed a novel view of concurrent computation in terms of resource passing, and designed a capability type system that unifies and generalizes mode systems and linearity systems.3. Interpreter technology for code mobility - We designed an intermediate code, called treecode, to realize code mobility between non-uniform nodes, and described its interpreter using Flat GHC
Research on Methodologies for Constructing Evolutionary Software

Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research

Project Year :

1997

-

2000

MIYAMOTO Eiichi, TAMAI Tetsuo, UEDA Kazunori, ARAKI Keijiro, TOGASHI Atsushi, FUTATSUGI Kokichi

　View Summary

1. We have developed a communication model which does not point particular receivers, which has enabled to evolve software in open and distributed systems efficiently.2. We measured source programs of objects, and extracted evolutional patterns in which line and method numbers in classes obey the negative diadic distribution.3. We made specifications into modules using the Algebraic specification language CafeOBJ, and then constructed the overall specification by synthesizing them. We also classified composite patterns into reusable one.4. By case studies, we analyzed the processes of model formation and construction and description of formal specification, reviewed features and meaning of formal specification description in evolutional processes of the description of system specifications.5. Based on strong mode systems in concurrent logic programming, we identified slight errors without specifications, and proposed a framework which corrects errors automatically.6. We defined system requirements based on propositon and predicate, proposed a method to convert them into formal specification, and proved its soundness and completeness.7. We developed a language to describe multi-agent systems which work in the environment of multi-processes and multi-threads and have migration facilities.8. We proposed "programming on cell" and "active programming" based π calculus and developed an exensible Java LSI processor to implement efficient programs.9. We analyzed the features of distributed data structures from the several different views and developed an efficient implementation for them
Architecture and Software for Real-time Access to Global Information

Project Year :

1997

-

2000
Applications of Strong Moding in Concurrent Logic Programming

Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research

Project Year :

1995

-

1998

UEDA Kazunori

　View Summary

The outstanding features of concurrent logic programming languages such as GHC (Guarded Horn Clauses) are the extreme simplicity of its communication and synchronization mechanisms and its flexibility in describing concurrency. To make the languages really practical, however, static analysis needs to play key roles both in programming and optimization.The head investigator had worked on the theoretical aspects of the static mode system (strong moding) for GHC and designed the algorithms for mode analysis. In this project, we worked on the practical aspects of strong moding and demonstrated its effectiveness from the following respects :1. Implementation of a mode analyzer - We implemented the mode analyzer klint for the concurrent logic language KL1 using KL1 itself as an implementation language. The system was revised several times until it could process large, real-life programs.2. Descriptive power under strong moding - We demonstrated, through the analysis of various real-life Eli programs, that concurrent logic languages with strong moding are as practical and expressive as those without strong moding.3. Program diagnosis based on strong moding - Strong moding turned out to be extremely useful for the static detection of program errors. We designed and implemented a set of algorithms for analyzing the errors of non-well-moded programs efficiently. Furthermore, we proposed a method of automated error correction and showed that it worked quite well for small program errors.4. Optimization based on strong moding - We demonstrated that, by using type and linearity information in addition to mode information, many of runtime operations such as tag checking could be eliminated, leading to performance not too different from that obtained by procedural programs
Integrated Parallel Processing

Project Year :

1996

-

1997

▼display all

Misc

SAT Evolution and Applications：7. Program Verification Using SMT Solvers

石井大輔, 上田和紀

情報処理 57 ( 8 ) 734 - 737 2016.07 [Invited]

Article, review, commentary, editorial, etc. (scientific journal)

　View Summary

プログラムの仕様記述，スケジューリングなど多くの応用問題は，命題論理で記述するよりも，整数の算術式や配列演算子など問題固有の記号を命題論理に埋め込んだ述語論理を用いたほうが記述しやすい．SMT（satis ability modulo theories）は，述語論理の充足可能性判定をSATソルバーと理論ソルバーを連携させて行うための技術である．本稿では，最近のSMTソルバーで用いられている求解技術を概観するとともに，応用事例として，SMTソルバーを利用して仕様付きプログラムの正当性を自動検証するプログラム検証技術を紹介する．

CiNii
特集『論理と推論技術の展開』の編集にあたって

上田和紀, 新田克己, 細部博史

コンピュータソフトウェア 25 ( 3 ) 1 - 1 2008.07

Article, review, commentary, editorial, etc. (scientific journal)
Symbolic Simulation of Parametric Hybrid Systems with Affine Arithmetic

33 321 - 331 2016.09

CiNii
Cooperation of Validated Numerics and Symbolic Formula Manipulation in Simulation of Hybrid Systems

115 ( 420 ) 93 - 98 2016.01

CiNii
Simulation with formula manipilation and interval arithmetic by HydLa implementation

29 1 - 4 2015

CiNii
Evaluation of Large-scale Graph Rewriting Model Checking Using Hash Compaction

YOSHIDA Taketo, ONUMA Masaru, UEDA Kazunori

IEICE technical report. Dependable computing 114 ( 156 ) 9 - 16 2014.07

　View Summary

Graph rewriting model checking is a verification method that determines whether a model described in a graph rewriting system satisfies required properties by exploring all reachable states. Graph rewriting has a high expressive power in representing information structures of models. This often results in the reduction of the number of states in model checking. On the other hand, graphs are heavyweight data structures in terms of both space and time. In this study, we implemented a Hash Compaction method to improve space and time efficiency of the LMNtal parallel model checker SLIM and measured its performance. Since Hash Compaction does not guarantee the reproduction of complete state space, we also studied and evaluated the effect of the accuracy of the hash function on the state space.

CiNii
ハイブリッドシステム制約言語HydLaの数式処理実行系へのアフィン演算の導入

松本翔太, 上田和紀

日本ソフトウェア科学会大会論文集 30 246 - 255 2013.09

CiNii
Optimized Canonical Graph Labeling Algorithm for Graph Rewriting Systems

30 515 - 534 2013.09

CiNii
Glucans : A parallel SAT solver with LBD-based sharing of learnt clauses

27 1 - 4 2013

CiNii
Optimization of a HydLa implementation using static analysis of constraints

27 1 - 4 2013

CiNii
Hyrose : A Symbolic Simulator of the Hybrid Constraint Language HydLa

29 377 - 392 2012.08

CiNii
Parallel Methods for Constraint Solving and Combinatorial Optimization

Philippe Codognet, Kazunori Ueda, Hiroshi Hosobe

NII Shonan Meeting Report ( 12-May ) 2012.05

Article, review, commentary, editorial, etc. (international conference proceedings)
Real-time Model Checking using Explicit-time Methods is SLIM

28 1 - 10 2011.09

CiNii
HyperLMNtal : an extension of a hierarchical graph rewriting language model

25 1 - 4 2011

CiNii
Evolution of the LMNtal runtime to a parallel model checker

27 1 - 17 2010.09

CiNii
Speedup of OWCTY Model Checking Algorithm using Strongly Connected Components

24 1 - 4 2010

CiNii
Tuning technique of the parallel LTL model checking with profiling

2009 ( 30 ) 1 - 7 2009.07

CiNii
Performance evaluation of the model checker Spin multi-core options on the large-scale memory environment

KOBAYASHI Fumiyoshi, UEDA Kazunori

71 23 - 24 2009.03

CiNii
State space search using LMNtal

23 1 - 4 2009

CiNii
Design and implementation of SLIM : a lightweight runtime of LMNtal

70 153 - 154 2008.03

CiNii
Franco-Japanese research collaboration on constraint programming

BENHAMOU Frederic, CEBERIO Martine, CODOGNET Philippe, HOSOBE Hiroshi, JERMANN Christophe, SATOH Ken, UEDA Kazunori

Progress in informatics : PI 3 59 - 65 2006.04

　View Summary

Constraint programming is an emergent technology that allows modeling and solving various problems in many areas such as artificial intelligence, computer programming, computer-aided design, computer graphics, and user interfaces. In this report, we recount the recent activities of research collaboration on constraint programming conducted by the authors and other researchers in France and Japan. First, we outline our joint research projects on constraint programming and then present the backgrounds, goals, and approaches of several research topics treated in the projects. Second, we describe the two Franco-Japanese Workshops on Constraint Programming (FJCP), which we held in Japan in October 2004 and in France in November 2005. We conclude with future prospects for collaboration between French and Japanese researchers in this area.

CiNii
萩谷昌己，横森貴共編：DNAコンピュータ，培風館 (2001)

上田和紀

人工知能学会誌 18 ( 1 ) 102 - 102 2003.01

Authorship：Lead author

Book review, literature introduction, etc.

CiNii
Concurrent Operations on Splay Trees

UEDA Kazunori, Kazunori Ueda, Dept.of Information and Computer Science Waseda University

16 ( 5 ) 478 - 483 1999.09

CiNii
プログラミング言語の新潮流

井田哲雄, 稲垣康善, 上田和紀, 米澤明憲, 筧捷彦

コンピュータソフトウェア 6 ( 3 ) 76 - 87 1989.07

Article, review, commentary, editorial, etc. (scientific journal)
第4回ロジックプログラミング国際会議に出席して

上田和紀, Kazunori Ueda, (財)新世代コンピュータ技術開発機構

コンピュータソフトウェア = Computer software 4 ( 4 ) 387 - 390 1987.10

CiNii

▼display all

Syllabus

Bachelor Thesis B

School of Fundamental Science and Engineering

2024 fall semester
Computer Science and Engineering Laboratory B [S Grade]

School of Fundamental Science and Engineering

2024 spring semester
Computer Science and Engineering Laboratory A [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Computer Science and Engineering Laboratory B

School of Fundamental Science and Engineering

2024 spring semester
Computer Science and Engineering Laboratory A (2)

School of Fundamental Science and Engineering

2024 fall semester
Bachelor Thesis B [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Bachelor Thesis B

School of Fundamental Science and Engineering

2024 fall semester
Project Research B

School of Fundamental Science and Engineering

2024 fall semester
Computer Science and Communications Engineering Laboratory [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Computer Science and Communications Engineering Laboratory

School of Fundamental Science and Engineering

2024 fall semester
Project Research A

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis A [S Grade]

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis A（Fall Semester）

School of Fundamental Science and Engineering

2024 fall semester
Reliable Software

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis A（Fall Semester）

School of Fundamental Science and Engineering

2024 fall semester
Bachelor Thesis A

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis B（Spring Semester）

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis B（Spring Semester）

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis A

School of Fundamental Science and Engineering

2024 spring semester
Programming Languages [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Programming Languages

School of Fundamental Science and Engineering

2024 fall semester
Programming B [S Grade]

School of Fundamental Science and Engineering

2024 spring semester
Programming B

School of Fundamental Science and Engineering

2024 spring semester
Reliable Software

School of Fundamental Science and Engineering

2024 spring semester
Artificial Intelligence and Logic

School of Fundamental Science and Engineering

2024 fall quarter
Bachelor Thesis B (Spring Semester)

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis B [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Bachelor Thesis A

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis B (Spring Semester)

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis A (Fall Semester)

School of Fundamental Science and Engineering

2024 fall semester
Bachelor Thesis B

School of Fundamental Science and Engineering

2024 fall semester
Bachelor Thesis A [S Grade]

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis A (Fall Semester)

School of Fundamental Science and Engineering

2024 fall semester
Communications and Computer Engineering Laboratory B [S Grade]

School of Fundamental Science and Engineering

2024 spring semester
Communications and Computer Engineering Laboratory B

School of Fundamental Science and Engineering

2024 spring semester
Communications and Computer Engineering Laboratory A [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Communications and Computer Engineering Laboratory A

School of Fundamental Science and Engineering

2024 fall semester
Reliable Software

School of Fundamental Science and Engineering

2024 spring semester
Artificial Intelligence and Logic

School of Fundamental Science and Engineering

2024 fall quarter
Reliable Software

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis B

School of Fundamental Science and Engineering

2024 fall semester
Project Research B

School of Fundamental Science and Engineering

2024 fall semester
Programming Languages

School of Fundamental Science and Engineering

2024 fall semester
Project Research A

School of Fundamental Science and Engineering

2024 spring semester
Programming B

School of Fundamental Science and Engineering

2024 spring semester
Bachelor Thesis A

School of Fundamental Science and Engineering

2024 spring semester
Graduation Thesis A (Spring) [S Grade]

School of Fundamental Science and Engineering

2024 spring semester
Computer Science and Communications Engineering Laboratory B

School of Fundamental Science and Engineering

2024 spring semester
Introduction to Computers and Networks

School of Fundamental Science and Engineering

2024 spring semester
Graduation Thesis A (Fall) [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Graduation Thesis B (Spring) [S Grade]

School of Fundamental Science and Engineering

2024 spring semester
Graduation Thesis B (Fall) [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Reliable Software

School of Fundamental Science and Engineering

2024 spring semester
Graduation Thesis A (Spring)

School of Fundamental Science and Engineering

2024 spring semester
Graduation Thesis B (Fall)

School of Fundamental Science and Engineering

2024 fall semester
Graduation Thesis A (Fall)

School of Fundamental Science and Engineering

2024 fall semester
Graduation Thesis B (Spring)

School of Fundamental Science and Engineering

2024 spring semester
Computer Science and Communications Engineering Laboratory A [S Grade]

School of Fundamental Science and Engineering

2024 fall semester
Computer Science and Communications Engineering Laboratory A

School of Fundamental Science and Engineering

2024 fall semester
Project Research Spring

School of Fundamental Science and Engineering

2024 spring semester
Project Research Fall

School of Fundamental Science and Engineering

2024 fall semester
Special Laboratory B in Computer Science and Communications Engineering

Graduate School of Fundamental Science and Engineering

2024 fall semester
Research on Parallel Knowledge Information Processing

Graduate School of Fundamental Science and Engineering

2024 full year
Special Laboratory B in Computer Science and Communications Engineering

Graduate School of Fundamental Science and Engineering

2024 fall semester
Advanced Project Study(Autumn)

Graduate School of Fundamental Science and Engineering

2024 fall semester
Advanced Project Study(Spring)

Graduate School of Fundamental Science and Engineering

2024 spring semester
Seminar on Parallel Knowledge Information Processing D

Graduate School of Fundamental Science and Engineering

2024 fall semester
Seminar on Parallel Knowledge Information Processing C

Graduate School of Fundamental Science and Engineering

2024 spring semester
Seminar on Parallel Knowledge Information Processing B

Graduate School of Fundamental Science and Engineering

2024 fall semester
Seminar on Parallel Knowledge Information Processing A

Graduate School of Fundamental Science and Engineering

2024 spring semester
Reliable Software

Graduate School of Fundamental Science and Engineering

2024 spring semester
Special Laboratory A in Computer Science and Communications Engineering

Graduate School of Fundamental Science and Engineering

2024 spring semester
Research on Parallel Knowledge Information Processing

Graduate School of Fundamental Science and Engineering

2024 full year
Research on Parallel Knowledge Information Processing

Graduate School of Fundamental Science and Engineering

2024 full year
Special Laboratory A in Computer Science and Communications Engineering

Graduate School of Fundamental Science and Engineering

2024 spring semester
Reliable Software

Graduate School of Fundamental Science and Engineering

2024 spring semester
Seminar on Parallel Knowledge Information Processing D

Graduate School of Fundamental Science and Engineering

2024 fall semester
Seminar on Parallel Knowledge Information Processing C

Graduate School of Fundamental Science and Engineering

2024 spring semester
Seminar on Parallel Knowledge Information Processing B

Graduate School of Fundamental Science and Engineering

2024 fall semester
Seminar on Parallel Knowledge Information Processing A

Graduate School of Fundamental Science and Engineering

2024 spring semester
Special Seminar B in Computer Science and Communications Engineering

Graduate School of Fundamental Science and Engineering

2024 fall semester
Special Seminar A in Computer Science and Communications Engineering

Graduate School of Fundamental Science and Engineering

2024 spring semester

▼display all

Overseas Activities

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

2000.09

-

2001.02

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

Sub-affiliation

Faculty of Science and Engineering Graduate School of Fundamental Science and Engineering

Research Institute

2022

-

2024

Waseda Research Institute for Science and Engineering Concurrent Researcher

Internal Special Research Projects

強力なデータ構造と並行性をもつ高水準言語の解析・実装技法の開拓

2023

　View Summary

本研究では，高い汎用性をもちながら通常の高水準言語が直接サポートしないグラフ構造を扱うプログラミング言語・モデリング言語のための新たな解析・実装技術の開拓に取り組んだ．対象言語として，階層グラフ書換え言語LMNtal，およびLMNtalのデータ構造をハイパーグラフに拡張したHyperLMNtalをとりあげた．解析技術については，通常の代数的データ型の範疇を超えるグラフ型の枠組みに対して，型の概念設計および解析の両面から検討を進めた．型の概念設計においては，グラフの書換え規則の型安全性検査を大幅に軽量化する型の差分概念を提案し，型の差分に基づく解析手法の構築を進めた．また，与えられたグラフが型の生成文法から生成できるかどうかの判定にtoken passingの考え方を導入するとともに，tokenの概念を拡張することで，threaded treeのような複雑なグラフ構造の解析が効率良くできることを示した．実装技術については，まず，木構造よりも低い結合度をもつ非連結グラフ構造も重要な用途をもつことから，非連結構造の書換えの実装最適化に取り組んだ．非連結構造の典型応用はタプルの多重集合の書換えだが，連結グラフのように辺を辿る探索ができないため探索に工夫が必要である．そこで，単調非減少な書換えルールに対して効率的に動作しかつC++等に変換可能なタプル書換えアルゴリズムを提案・評価した．索引構造をはじめとするさまざまな工夫によって，計測例題に対して1000倍以上の高速化に成功した．また，再帰的生成規則で定義したグラフパターンのマッチング機能を備えたCSLMNtal言語について，プログラムの実行過程で繰り返されるパターンマッチングを素朴に実装した場合に発生する重複作業を削減するマッチングアルゴリズムを設計し，実際に計算量が改善されることを確認した．
汎用かつ強力なデータ構造と実行機能をもつ高水準言語の基礎研究

2022 山本直輝

　View Summary

複雑な接続関係とその変化をグラフ構造とその書換え作業として表現する能力は，プログラミング言語とモデリング言語の双方にとって重要である．しかしこれまでの言語では，リストや木構造よりも複雑な構造の簡潔な表現と安全な操作，それらを支える型体系の開拓が不十分であった．本研究では，グラフ書換え言語LMNtalのためのグラフ型概念およびグラフ型検査の枠組みを構築して，その性質を多角的に検討した．最大の特徴は，グラフの型を表現する生成文法をLMNtalの書換え規則の形で表現する点にある．構築した型検査アルゴリズムを実装して，さまざまなグラフ構造に対する実際的な操作の型検査が可能であることを示した．
高水準モデリング言語の高機能な実行・検証系

2022

　View Summary

プログラミングにおいてグラフ構造は強力で一般性の高いデータ構造である．グラフ構造は命令型言語ではヒープ上のポインタ構造に対する破壊的代入として扱われるが，その正当性検証は容易でない．一方，純粋関数型言語で一般のグラフ構造を扱う方法は未確立であった．そこで本研究では，新たな純粋関数型言語λGTの設計を行い，概念実証のための処理系を構築した．λGTはグラフをimmutableな第一級データ構造として表現し，グラフ変換計算モデルに基づくパターンマッチングによって分解合成を行う．λGTの構文と意味論を厳密に定義するとともに，λGTの型体系としてFGTを設計して型付け規則を与えた．
高水準モデリング言語の特性を活かす高機能な実行・検証系

2021

　View Summary

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

2021

　View Summary

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

2017

　View Summary

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

2007 石井　大輔

　View Summary

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

2004 加藤　紀夫

　View Summary

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

1998

　View Summary

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

1996

　View Summary

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

1995

　View Summary

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

▼display all