| Budget Amount *help |
¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000)
Fiscal Year 2014: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2013: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2012: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Outline of Final Research Achievements |
Formal verification is a technique to guarantee the correctness of software with a high level of confidence. Yet, when software is written in low-level programming languages such as C or assembly, there are so many details that it is difficult in practice to perform such a verification. With embedded software as an objective, we formalize a model and a logic for C that takes platform-dependent details into account. More precisely, to allow for the verification of programs mixing C and assembly, we developed in the Coq proof-assistant a formal library whose validity is assessed by substantial case-studies.
|
