Formal Verification System by using Hardware Compiler Fusioning of Theorem Prover and Model Checker on the Grid Environment
Project/Area Number |
23500174
|
Research Category |
Grant-in-Aid for Scientific Research (C)
|
Allocation Type | Multi-year Fund |
Section | 一般 |
Research Field |
Intelligent informatics
|
Research Institution | Shinshu University |
Principal Investigator |
|
Project Period (FY) |
2011 – 2013
|
Project Status |
Completed (Fiscal Year 2013)
|
Budget Amount *help |
¥5,200,000 (Direct Cost: ¥4,000,000、Indirect Cost: ¥1,200,000)
Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2012: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
Fiscal Year 2011: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
Keywords | 探索・論理・推論アルゴリズム / プルーフチェッカ / 定理証明器 / コンパイラ / 関数型言語系 |
Research Abstract |
A theorem prover that implements to the grid computing environment fuses the output hardware compiler target implementation various code. To build a formal verification system which is consistent high to function downstream from the upstream, thereby dramatically improving the ability for verification of asynchronous parallel circuit system. The configuration informations of the target circuit has been described on the functional language system. As compiler output of the language system, we can get the target implementation code and the type of proof to proof checker. The target circuit has been modeled by message passing parallel computer based on the 4-valued logic two-wire model of asynchronous logic gate element. Finally, proof checker can verify its correctness proof by using of the circuit connection.
|
Report
(4 results)
Research Products
(45 results)