Decision procedures of modal logics and their application to software verification

点击翻译按钮获取中文摘要

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.