2008 Fiscal Year Final Research Report Summary
Type Theory for Software Safety
| Project/Area Number |
17300003
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
KOBAYSHI Naoki Tohoku University, Graduate School of Information Sciences, Professor (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SUMII Eijiro Tohoku University, Graduate School of Information Sciences, Associate Professor (00333550)
IGARASHI Atsushi Kyoto University, Graduate School of Informatics, Associate Professor (40323456)
TERAUCHI Tachio Tohoku University, Graduate School of Information Sciences, Assistant Professor (70447150)
|
|---|
| Project Period (FY) |
2005 – 2007
|
| Keywords | program verification / program analysis / type theory / functional programs / concurrent programs / information flow analysis |
|---|
| Research Abstract |
The purpose of this project was to enhance software verification techniques based on formal methods such as type theories. The primary goal was to refine and extend our previous type-based verification techniques so that they can be used for verification of realistic programs.
The main results are summarized as follows. For each topic, we have implemented a prototype verification system and confirmed the effectiveness of the verification technique.
1. Verification methods for functional programs
A main shortcoming of our previous type-based technique for resource usage verification was that it did not properly handle advanced language mechanisms such as exceptions. We have extended the previous resource usage verification technique to deal with exceptions. We have also devised an (incomplete) algorithm to infer dependent types, to enable automatic but more precise program analysis than previous methods.
2. Verification methods for concurrent programs
The main shortcomings of our previous verification method were that it was too imprecise and that it did not handle some common primitives such as reference cells and interrupts. To address the former issue, we have integrated our previous type-based method with model-checking techniques. For the latter issue, we have developed verification methods for a C-like language with interrupts and reference cells.
3. Information Flow Analysis
We have integrated a type-based technique for information flow analysis with a mode-checking technique. The resulting analysis is more precise than previous type-based techniques, and more efficient than previous model-checking techniques for information flow analysis.
|
Research Products
(25 results)
