An Algebraic Semantics of Predicate Abstraction for PML

DOI
  • 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

Details 詳細情報について

  • CRID
    1390282679713175936
  • NII Article ID
    130004892130
  • DOI
    10.11309/jssst.26.2_147
  • ISSN
    02896540
  • Data Source
    • JaLC
    • CiNii Articles
  • Abstract License Flag
    Disallowed

Report a problem

Back to top