Verification of Multi-thread Programs via Linear Programming
| Project/Area Number |
20700019
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
TERAUCHI Tachio 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| Project Period (FY) |
2008 – 2010
|
| Project Status |
Completed (Fiscal Year 2010)
|
| Budget Amount *help |
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2010: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2009: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2008: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | ソフトウェア検証 / プログラム言語 / 型推論 / 権限計算 / 線形計画法 / 型理論 |
|---|
| Research Abstract |
We propose a software verification framework based on the formalism of fractional capabilities thatstatically (i.e., at compile time) and automatically checksthatcertain bad things (e.g., data races) never happenin concurrent programs. The key to the success is the reduction of fractional capability calculito the problem of linear programming.
|
Report
(4 results)
Research Products
(20 results)
