An Algebraic Semantics of Predicate Abstraction for PML
-
- KINOSHITA Yoshiki
- Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST)
-
- NISHIZAWA Koki
- Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST) Department of Information Systems, Faculty of Environmental and Information Studies, Tottori University of Environmental Studies
Bibliographic Information
- Other Title
-
- PMLのための述語抽象化の代数意味論
Abstract
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.
Journal
-
- Computer Software
-
Computer Software 26 (2), 147-156, 2009
Japan Society for Software Science and Technology
- Tweet
Details 詳細情報について
-
- CRID
- 1390282679713175936
-
- NII Article ID
- 130004892130
-
- ISSN
- 02896540
-
- Data Source
-
- JaLC
- CiNii Articles
-
- Abstract License Flag
- Disallowed