2011 Fiscal Year Final Research Report
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
|
| 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.
|
