An Algebraic Semantics of Predicate Abstraction for PML
スポンサーリンク
概要
- 論文の詳細を見る
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.
著者
-
Nishizawa Koki
Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST)
-
Kinoshita Yoshiki
Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST)