|
|
キノシタ ヨシキ
Kinoshita Yoshiki 木下 佳樹 所属 神奈川大学 情報学部 計算機科学科 神奈川大学大学院 理学研究科 理学専攻(情報科学領域) 職種 教授 |
|
言語種別 | 日本語 |
発行・発表の年月 | 2009/04 |
形態種別 | 学術雑誌 |
査読 | 査読あり |
標題 | An algebraic semantics of predicate abstraction for PML |
執筆形態 | 共著 |
掲載誌名 | Computer Software (Iwanami shoten) |
巻・号・頁 | 26(2),147-156頁 |
著者・共著者 | Koki Nishizawa and Yoshiki Kinoshita |
概要 | We give a semantics of abstraction in PML (Pointer Manipulation Language) given by Takahashi et al.. This is an instance of unifying theory for abstraction of reactive systems given by the second author et al., as every model of PML induces a model of Rμ, a modal logic with fixpoints studied by the second author. It gives the proof of the correctness of predicate abstraction used in MLAT. |