Decision procedures of modal logics and their application to software verification
| Project/Area Number |
21500006
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | National Institute of Informatics (2010-2011)
The University of Tokyo (2009) |
|---|
Principal Investigator |
TANABE Yoshinori 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (60443199)
|
|---|
| Project Period (FY) |
2009 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000)
Fiscal Year 2011: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2009: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | 様相論理 / 決定手続き / ソフトウェア検証 / モデル検査 / 充足可能性 / 様相μ計算 / min-plus代数 / 法定手続き |
|---|
| Research Abstract |
We built a theory for applying modal logics to verification of programs that manipulate pointers, especially for techniques to judge the termination. It includes the weakest precondition and the strongest postcondition of operations of Kripke structures, and an extension of the semantics of modal mu-calculi. In the latter, we built a semantics in which truth values are members of min-plus algebra N-infty, and gave solutions to the model-checking problem and the satisfiability judgment problem with this semantics.
|
Report
(4 results)
Research Products
(20 results)
