京都橘大学教員情報

（最終更新日：2023-04-03 15:35:54）

  ハマグチ　キヨハル   HAMAGUCHI Kiyoharu
  濵口　清治
   所属   京都橘大学工学部情報工学科

職種教授

■ 学内役職・委員

2023/04/01～

京都橘大学工学部長

■ 学歴

1.	1993/03 (学位取得)	京都大学博士〈工学〉
2.	1987/04～1989/03	京都大学大学院工学研究科情報工学専攻修士課程修了

■ 専門分野

計算基盤　（キーワード：計算機システム、計算機システム・ネットワーク、デジタル回路の設計検証、論理関数処理技術）

■ 所属学会

1.	1997/02～	Association for Computing Machinery （ACM）
2.	1995/03～	Institute of Electrical and Electronical Engineers（IEEE）
3.	1987/02～	電子情報通信学会
4.	1987/01～	情報処理学会
5.	2003/04～	∟ システムLSI設計技術研究会運営委員会委員
6.	2005/04～2007/03	∟ システムLSI設計技術研究会幹事
7.	2005/04～2007/03	∟ 組込みシステム研究会運営委員会委員
8.	2016/04～2018/03	∟ システムLSI設計技術研究会主査
5件表示
全件表示(8件)

■ 著書

1.	2006/10	著書	『システムLSI設計工学』オーム社（共著）
2.	1996/06	著書	『超並列計算講義』共立出版（共著）

■ 論文

1.	2023/06	学術論文	「Parallelizing Random and SAT-based Verification Processes for Improving Toggle Coverage」 IPSJ Transactions on System and LSI Design Methodology Information Processing Society of Japan 16:45-53 （単著）
2.	2018/07	学術論文	「Applying an SMT Solver to Coverage-driven Design Verification(カバレッジ駆動型設計検証への SMT ソルバの適用)」 IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences Vol.E101-A(No.07):pp.1053-1056 （単著）
3.	2017/07	学術論文	「Coverage-driven Design Verification Using a Diverse SAT Solver(ダイバースSATソルバーを用いたカバレッジ駆動型設計検証)」 IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences Vol.E100-A(No.07):pp.1481-1487 （共著）
4.	2011/08	学術論文	「Symbolic Discord Computation for Efficient Analysis of Message Sequence Charts(メッセージシークエンスチャートの効率的な解析のための記号ディスコード計算)」 IPSJ Transactions on System LSI Design Methodolog Vol.4:pp.210-221 （共著）
5.	2010/08	学術論文	「Approximate Model Checking using a Subset of First-Order Logic(第一階述語論理の部分集合を用いた近似的モデル検査)」 IPSJ Transactions on System LSI Design Methodology Vol.3:pp.268-282 （共著）
6.	2010/02	学術論文	「Approximate Invariant Property Checking Using　Term-Height Reduction for a Subset of First-Order Logic(第一階述語論理の部分集合に対する項の高さ縮減を用いた近似的な不変条件検査)」 IPSJ Transactions on System LSI Design Methodology Vol.3:pp.105-117 （共著）
7.	2009/02	学術論文	「Checker Generation of Assertions with Local Variables for Model Checking(モデル検査のための局所変数を含むアサーションに対するチェッカ生成)」 IPSJ Transactions on System LSI Design Methodology Vol.2:pp.80-92 （共著）
8.	2007/12	学術論文	「A Monitor Generation Method for Formal Monitor-based Verification Considering Input Constraints(入力制約を考慮した形式的モニターベース検証のためのモニタ生成手法)」 Systems and Computers in Japan - Part III Vol.90(No.12):pp.19-26 （共著）
9.	2007/12	学術論文	「Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints(等式制約下での等号と無解釈関数を持つ論理体系に対する充足可能性判定)」 IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences Vol.E90-A(No.12):pp.2778-2789 （共著）
10.	2006/04	学術論文	「モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法」電子情報通信学会論文誌 D-I Vol.J89-D(No.4):pp.674-682 （共著）
11.	2006/03	学術論文	「Expressive Power of Quantum Pushdown Automata with Classical Stack Operations under the Perfect-Soundness Condition(完全健全性条件のもとでの古典的なスタック操作を有する量子プッシュダウンオートマトンの表現能力について)」 IEICE Trans. on Information and Systems Vol.E89-D(No.3):pp.1120-1127 （共著）
12.	2004/03	学術論文	「Symbolic Simulation Heuristics for High-Level Hardware Descriptions Including Uninterpreted Functions(無解釈関数を含む高位ハードウェア記述に対する記号シミュレーションのための発見的手法)」 IEICE Trans. on Fundamentals of Electronics, Communications and Computer Science Vol.E87-D(No.3):pp.637-641 （単著）
13.	2002/10	学術論文	「Verifying Signal-Transition Consistency of High-Level Designs Based on Symbolic Simulation (記号シミュレーションに基づく高位設計の信号変化等価性の検証)」 IEICE Trans. on Fundamentals of Electronics,Communications and Computer Sciences Vol.E85-D(No.10):pp.1587-1594 （共著）
14.	2002/02	学術論文	「On the Power of Non-deterministic Quantum Finite Automata(非決定量子有限オートマトンの表現能力について)」 IEICE Trans. on Information and Systems Vol.E85-D(No.2):pp.327-332 （共著）
15.	2000/01	学術論文	「クロネッカー式関数決定グラフの最適展開規則選択問題の計算複雑度」電子情報通信学会論文誌（D-I） J83-D-I巻(1号):pp.115-120 （共著）
16.	1999/11	学術論文	「A Partially Explicit Method for Efficient Symbolic Checking of Language Containment(効率的な言語包含の記号検査のための部分明示手法)」 IEICE Trans. on Fundamentals of Electroni Communications and Computer Scienc vol.E82(No.11):pp.2455-2464 （共著）
17.	1999/05	学術論文	「An Exponential Lower Bound on the Size of a Binary Moment Diagram Representing Integer Division(整数除算を表現する二分モーメントグラフのサイズに関する指数下界)」 IEICE Trans. on Fundamentals of Electronics、 Communications and Computer Sciences Vol.E82-A(No.5):pp.756-766 （共著）
18.	1999/05	学術論文	「しきい値関数を表す共有2分決定グラフの最適な変数順序付けの計算複雑度」電子情報通信学会論文誌(D-I) Vol.J82-D-I巻(No.5):pp.595-602 （共著）
19.	1997/10	学術論文	「Manipulation of Large-Scale Polynomials Using Binary Moment Diagrams(二分モーメントグラフを用いた大規模多項式の操作)」 IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences Vol.E80-A(No.10):pp.1774-1781 （共著）
20.	1997/02	学術論文	「Another Look at LTL Model Checking(LTLモデル検査再訪)」 Formal Methods in System Design Vol.10:pp.47-71 （共著）
21.	1996/04	学術論文	「The Complexity of the Optimal Variable Ordering Problems of a Shared Binary Decision Diagram(共有二分決定グラフに対する最適変数順序付け問題の計算複雑さ)」 IEICE Trans. on Information and System Vol.D79-D(No.4):pp.271-281 （共著）
22.	1993/10	学術論文	「Compact Test Sequences for Scan-Based Sequential Circuits(スキャンベース順序回路に対するコンパクトなテスト系列生成)」 IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences,Optimal Vol.E76-A(No.10):pp.1676-1683 （共著）
23.	1992/10	学術論文	「Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic(分岐時間正則時相論理に対する記号モデル検査に基づく順序機械の形式的設計検証)」 IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences Vol.E75-A(No.10):pp.1220-1229 （共著）
24.	1992/09	学術論文	「∞ Regular Temporal Logic and Its Model Checking Problem(∞正則時相論理とそのモデル検査問題)」 Theoretical Computer Science Vol.103:pp.191-204 （共著）
25.	1992/04	学術論文	「形式的設計検証のための分岐時間正則時相論理」情報処理学会論文誌第33巻(第4号):pp.405-414 （共著）
26.	1990/06	学術論文	「有限オートマトンと表現等価な正則時相論理とその論理設計検証への応用」情報処理学会論文誌第31巻(第7号):pp.1134-1145 （共著）
27.	1989/03	学術論文	「正則時相論理の充足可能性判定アルゴリズム」情報処理学会論文誌第30巻(第3号):pp.366-374 （共著）
5件表示
全件表示(27件)

■ その他

1.	2005/01	その他（解説・一般記事）	大規模回路設計に対するフォーマル仕様記述・検証技術の現状と動向電子情報通信学会誌第88巻(第1号):pp.35-39 （単著）
2.	1994/08	その他（解説・一般記事）	論理関数処理に基づく形式的検証手法情報処理第35巻(第8号):pp.710-718 （共著）
3.	1993/10	その他（解説・一般記事）	ぼくらのマイクロプロセッサ開発記 bit Vol.25 No.10 pp.21-33, Vol.25 No.11 pp.47-58, Vol.25 No.12 pp.39-51, Vol.26 No.1 （共著）

■ 学会発表

1.	2021/03	Error Detection Capacity of SAT-based Coverage-driven Design Verification（2021 Synthesis and Simulation Meeting and International Interchange）
2.	2019/10	Parallelizing SAT-based Coverage-Driven Design Verification（2019 Synthesis and Simulation Meeting and International Interchange）
3.	2019/05	正規表現照合器の複数サイクル状態遷移に着目したFPGA実装とその評価（LSIとシステムのワークショップ2019）
4.	2018/03	Applying Bayesian Network-Based Machine Learning to Regression Design Verification(リグレッション設計検証に対するベイジアンネットワークベースの機械学習の適用)（2018 Synthesis and Simulation Meeting and International Interchange）
5.	2018/03	Extracting Hardware Assertions Including Word-level Relations over Multiple Clock Cycles(多クロックサイクルにわたるワードレベルの関係を含むハードウェアアサーションの抽出)（2018 International Symposium on Quality Electronic Design）
6.	2018/01	多クロックサイクルのワードレベルの関係を含むハードウェアアサーションの自動抽出（情報処理学会システムLSI設計技術研究会(2017-SLDM-182-27)）
7.	2016/09	ベイジアンネットワークの機械学習を利用したリグレッション検証の効率改善（情報処理学会システムLSI設計技術研究会 DAシンポジウム2016）
8.	2016/03	Finding Effective Simulation Patterns for Coverage-Driven Verification Using Deep Learning(深層学習を用いたカバレッジ駆動型検証に対する効率的なシミュレーションパターンの発見手法)（2016Synthesis and Simulation Meeting and International Interchange）
9.	2013/08	FPGAにおける乗算回路の低電力メモリベース設計（情報処理学会システムLSI設計技術研究会）
10.	2012/08	動作レベル回路設計記述の等価性判定における複数の論理体系を利用した抽象化（情報処理学会システムLSI設計技術研究会 DAシンポジウム2012）
11.	2011/03	トランザクション識別子を伴うバスプロトコル間の変換器自動生成手法（情報処理学会システムLSI設計技術研究会(2010-SLM-149)）
12.	2010/11	MAP Inference on ZDD-based Representation of Bayesian Networks(ベイジアンネットワークのZDD表現に対する最大事後確率推論)（International Workshop on Advanced Methodologies for Bayesian Networks）
13.	2010/03	メッセージ・シークエンス・チャートに対する SAT ソルバーを用いたディスコード計算手法（情報処理学会システムLSI設計技術研究会(2009-SLDM-144-63)）
14.	2009/12	第一階述語論理のサブクラスに対する近似的モデル検査アルゴリズム（情報処理学会システムLSI設計技術研究会(2009-SLDM-142-9)）
15.	2009/10	SMT ソルバーを利用した近似的な非有界モデル検査アルゴリズムにおける複数の論理体系の組み合わせ手法（査読付）（組み込みシステムシンポジウム2009）
16.	2009/08	バースト転送を考慮したバスプロトコル変換器の自動合成（情報処理学会システムLSI設計技術研究会、DAシンポジウム2009）
17.	2009/07	Exploiting Global Structures in Bayesian Network Compilation by Zero-suppressed BDDs(ゼロサプレス二分決定グラフによるベイジアンネットワークのコンパイレーションにおける全体構造の利用)（International Conference on Inductive Logic Programming）
18.	2009/07	Monolithic and Partial Compilation Methods for Probabilistic Inference of Bayesian Networks using ZBDDs(ZBDDを用いたベイジアンネットワークの確率推論に対する全体および部分的コンパイレーション手法)（International Workshop on Data-Mining and Stastical Science）
19.	2008/11	Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic(第一階述語論理の部分集合に対する項の高さ縮減を用いた近似的な不変条件検査)（International Conference on Automated Technology for Verification and Analysis）
20.	2007/11	第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム（情報処理学会システムLSI設計技術研究会､DAシンポジウム2007）
21.	2007/10	Encoding Assertions with Dynamic Local Variables for Bounded Property Checking(有界プロパティ検査のための動的変数を含むアサーションの符号化)（Synthesis and Simulation Meeting and International Interchange）
22.	2006/11	動的局所変数を含むアサーションに対する限定モデルチェッキング（情報処理学会システムLSI設計技術研究会､情報処理学会研究報告2006(SLDM-127)）
23.	2006/11	同値制約を考慮した第一階述語論理の決定可能なサブクラスによる等価性判定（情報処理学会システムLSI設計技術研究会､情報処理学会研究報告2006(SLDM-127)）
24.	2006/04	Satisfiability Checking under Equivalence Constraints for a Decidable Subclass of First-Order Logic(第一階述語論理の決定可能な部分クラスに対する等式制約下での充足可能性判定)（Synthesis and Simulation Meeting and International Interchange）
25.	2006/01	[チュートリアル] 'Basics and Practice of Current Functional Verification Methods (近年の機能検証手法の基本と実際)（11th Asia and South Pacific Design Automation Conference (ASP-DAC2006)）
26.	2006/01	第一階述語論理のサブクラスを利用したブール関数レベルの等価性判定手法（情報処理学会システムLSI設計技術研究会(2006-SLDM-123)）
27.	2005/10	モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法（情報処理学会システムLSI設計技術研究会(2005-SLDM-121)）
28.	2005/05	Automatic Monitor Generation from Regular Expression based Specifications for Module Interface Verification(モジュール間インターフェースの検証のための正則表現に基づく仕様からの自動モニタ生成)（International Symposium on Circuits and Systems 2005）
29.	2005/03	第一階述語論理の決定可能なサブクラスに対する同値制約を考慮した充足可能性判定（電子情報通信学会CPSY研究会(CPSY2004-113)）
30.	2005/01	アサーションベース検証の基礎とそのねらい（電子情報通信学会VLSI設計技術研究会）
31.	2004/11	Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas(ブール式の代入を使った限量子を含まない等号付き第一階述語論の恒真性判定)（Proceedings of the 2nd International Synposium on Automated Technology for Verification and Analysis ATVA 2004）
32.	2004/10	Behavioral Model Construction for Formal Verification of Advanced On-Chip Bus Protocols(高性能オンチップ・バスプロトコルの形式的検証のための動作モデルの生成)（Synthesis and Simulation Meeting and International Interchange）
33.	2004/10	正規表現による仕様記述に対する効率的な形式的検証のための状態割り当てアルゴリズム（情報処理学会関西支部支部大会）
34.	2004/07	ブール式への置換を利用した限量子を含まない等号付第一階述語論理式の恒真性判定手法（情報処理学会システムLSI設計技術研究会､DAシンポジウム2004）
35.	2003/10	Design Verification Technologies for System-on-Chip (システムオンチップに対する設計検証技術)（Japan-Taiwan Microelectronics International Symposium -LSI Design Methodology -）
36.	2003/07	IPインターフェースプロトコルのモデル化と検証手法の提案（情報処理学会システムLSI設計技術研究会､ DAシンポジウム2003）
37.	2001/11	Symbolic Simulation Heuristics for High-Level Design Descriptions with Uninterpreted Functions(無解釈関数を含む高位ハードウェア記述に対する記号シミュレーションに関する発見的手法)（IEEE International High Level Design Validation and Test Workshop2001）
38.	2000/11	Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs(高位設計の検証のための信号変化等価性の記号検査)（Formal Methods in Computer Aided Design）
39.	2000/07	Ordered Quantum Branching Programs Are More Powerful Than Ordered Probabilistic Branching Programs Under Bounded-width Restriction(幅が限定された順序付き量子分岐プログラムと順序付き確率分岐プログラムの能力比較について)（International Computing and Combinatorics Conference）
40.	2000/04	Bounded Model Checking for Design Verification of Abstract State Machines(抽象的な状態機械の設計検証のための有界モデル検査)（Synthesis and Simulation Meeting and International Interchange）
41.	2000/03	1回読み定数幅制約下での量子ブランチングプログラムと確率ブランチングプログラムの計算能力の比較（電子情報通信学会コンピュテーション研究会）
42.	1998/10	A Partially Explicit Method for Efficient Symbolic Checking of Language Containment(効率的な言語包含の記号検査のための部分的明示手法)（Synthesis and Simulation Meeting and International Interchange）
43.	1998/05	An Exponential Lower Bound on the Size of a Binary Moment Diagram Representing Division(除算を表現する二分モーメントグラフのサイズの指数下界)（International Workshop on Post-Binary ULSI Systems）
44.	1997/10	二分モーメントグラフによる除算表現の大きさの指数下界（電子情報通信学会コンピュテーション研究会(COMP97-53)）
45.	1996/03	Manipulation of Large-Scale Polynomials Using Binary Moment Diagrams(二分モーメントグラフを用いた大規模多項式の操作)（電子情報通信学会 1996年総合大会 D-6）
46.	1996/03	形式的手法によるキャッシュ・プロトコルの設計検証 -- 超並列計算機 JUMP-1 への適用例 --（電子情報通信学会計算機アーキテクチャ研究会）
47.	1995/12	Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits(算術演算回路検証のための二分モーメントグラフの効率的な構成方法)（情報処理学会設計自動化研究会）
48.	1995/11	Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits(算術演算回路検証のための二分モーメントグラフの効率的な構成方法)（International Conference on Computer-Aided Design）
49.	1994/06	Another Look at LTL Model Checking(LTLモデル検査再訪)（Conference on Computer-Aided Verification）
50.	1993/12	The Complexity of the Variable Ordering Problems of Shared Binary Decision Diagrams(共有二分決定グラフの変数順序付け問題の計算複雑さ)（International Symposium on Algorithms and Computation）
51.	1993/08	Formal Verification of Single Phase Behavior of KUE-CHIP2 Microprocessor(KUE-CHIP2 の単一フェーズ動作の形式的検証)（International Conference on CAD and Computer Graphics）
52.	1993/04	論理関数処理と形式的検証について（回路とシステム軽井沢ワークショップ）
53.	1993/03	組合せ回路の等価性判定問題の計算量と回路構造の関係について（電子情報通信学会春季全国大会 SA-2-3）
54.	1993/03	論理関数処理によるスキャン設計を考慮した順序回路に対するテスト生成（電子情報通信学会春季全国大会 SA-2-7）
55.	1993/03	順序機械の設計検証における BDD 処理に適した逆像計算法（電子情報通信学会春季全国大会 SA-2-5）
56.	1992/07	Design Verification of Asynchronous Sequential Circuits Using Symbolic Model Checking(記号モデル検査を用いた非同期式順序回路の設計検証)（International Symposium on Logic Synthesis and Microprocessor Architecture）
57.	1992/06	Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic(分岐時間正則時相論理を用いたマイクロプロセッサの設計検証)（Workshop on Computer-Aided Verification）
58.	1992/04	Formal Verification of Sequential Circuits Based on Symbolic Model Checking for Branching Time Regular Temporal Logic(分岐時間正則時相論理に対する記号モデル検査を用いた順序回路の形式的検証)（Synthesis and Simulation Meeting and International Interchange）
59.	1992/03	分岐時間正則時相論理によるマイクロプロセッサーの形式的設計検証（電子情報通信学会春季全国大会）
60.	1991/07	Formal Verification of Speed-Dependent Asynchronous Circuits Using Symbolic Model Checking of Branching Time Regular Temporal Logic(分岐時間正則時相論理の記号モデル検査を用いた速度依存型非同期式回路の形式的検証)（Workshop on Computer-Aided Verification）
61.	1991/07	Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification(順序機械の検証のための Computation Tree Logic のベクトル化記号モデル検査)（Workshop on Computer-Aided Verification）
62.	1991/03	共有二分決定グラフを用いた分岐時間正則時相論理による順序機械の設計検証（電子情報通信学会春季全国大会）
63.	1990/06	Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity(線形時間モデル検査のための分岐時間正則時相論理)（Workshop on Computer-Aided Verification）
64.	1990/06	Vectorized Model Checking for Computation Tree Logic(Computatation Tree Logic に対するベクトル化モデル検査)（Workshop on Computer-Aided Verification）
65.	1990/03	正則時相論理のモデルチェック法の改良と設計検証への適用（情報処理学会第40回全国大会）
66.	1990/03	線形時間のモデルチェッキングアルゴリズムを持つ正則時相論理と変数代入機構による拡張（情報処理学会第40回全国大会）
67.	1989/03	正則時相論理による論理設計検証システム（電子情報通信学会春季全国大会）
68.	1989/03	正則時相論理に基づく時間の抽象度の異なるレベル間での形式的検証（電子情報通信学会春季全国大会）
69.	1988/03	正則時相論理による順序機械の設計検証（電子情報通信学会春季全国大会）
70.	1987/03	正則時相論理の充足可能性判定アルゴリズム（電子情報通信学会春季全国大会）
5件表示
全件表示(70件)

■ 科研費・外部資金等

1.	2018/04～	SATソルバと機械学習手法を融合した自動設計検証に関する研究基盤研究(C)
2.	2013/04～2017/03	機械学習を用いたカバレッジ駆動型ハードウェア検証の効率化に関する研究基盤研究(C)
3.	2010/04～2013/03	フォーマル手法およびシミュレーション手法の統合によるハードウェア検証の効率化基盤研究(C)
4.	2007/04～2010/03	高位ハードウェア設計記述に対するモデル検査手法の研究基盤研究(C)
5.	2004/04～2007/03	高位ハードウェア設計記述に対する等価性判定手法の研究基盤研究(C)
6.	2001/04～2003/03	動作レベルおよびレジスタ転送レベルのハードウェア記述に対する形式的検証手法の研究若手研究(A)
7.	1998/04～2000/03	ハードウェアの機能レベル設計に対する形式的検証手法に関する研究奨励研究(A)
8.	1996/04～1997/03	等式論理による機能レベル設計の形式的検証に関する研究奨励研究(A)
9.	1995/04～1997/03	マイクロプロセッサの形式的論理設計検証システムの試作研究基盤研究(A)
10.	1995/04～1996/03	規則性を持つ大規模な有限状態機械の形式的設計検証に関する研究奨励研究(A)
11.	1994/04～1995/03	マイクロプロセッサの形式的仕様記述・検証に関する研究奨励研究(A)
12.	1993/04～1995/03	時相理論に基づく論理設計の形式的検証システムの試作研究試験研究(B)
13.	1993/04～1995/03	論理関数高速処理機構に関する基礎的研究一般研究(B)
14.	1992/04～1994/03	計算機工学・集積回路工学教育研究用マイクロプロセッサの開発試験研究(B)
15.	1992/04～1993/03	分岐時間正則時相論理による論理回路の仕様記述・設計検証手法の研究奨励研究(A)
5件表示
全件表示(15件)

■ 受賞学術賞

1.	2001/04	電子情報通信学会情報・システムソサイエティ論文賞（先見論文） (The Complexity of the Optimal Variable Ordering Problemsof a Shared Binary Decision Diagram)
2.	1995/10	情報処理学会山下記念研究賞受賞 (Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits)

■ 委員会・協会等

2013/04～2015/03

日本学術振興会科学研究費事業審査委員