2010 Fiscal Year Final Research Report
Design verification method of massively parallel arithmetic unit combined using a functional language and the Grid computing system
| Project/Area Number |
20500130
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
WASAKI Katsumi Shinshu University, 工学部, 教授 (70271492)
|
|---|
| Project Period (FY) |
2008 – 2010
|
| Keywords | 探索・論理・推論アルゴリズム / プルーフチェッカ |
|---|
| Research Abstract |
The main outcome of this project is to improve the ability to verify that the parallel system. For instance, A proof checker (mathematical theorem prover) has been implemented on the network environment. The target information of circuit configurations describes using a functional language. The output code from the compiler uses to prove the sequence of proof expressions by proof checker. To achieve parallelism, this research project introduced a representation model by Petri net. The "pipeline" mechanism is used as a computational model to explain. Next, this project developed a meta hardware compiler based on a functional programming language. Finally, several formal verification tools have tested in the term of project.
|
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] 整数有限列上の加算・乗算アルゴリズムの正当性証明に関する検討2009
Author(s)
伊藤比佐志, 和崎克己
Organizer
日本Mizar学会2009年春期総会予稿集(Proceedings of the Technical Symposium and General Assembly of Mizar JAPAN),4,(1),6pages
Place of Presentation
信州大学長野(工学)キャンパス総合研究棟
Year and Date
2009-06-19
-
-
-
[Remarks] ホームページ等
-
-
-
