Enhancing modular OO verification with separation logic

Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Abstract

    Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this.
    Original languageEnglish
    Title of host publicationProceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008
    PublisherACM
    Pages87-99
    ISBN (Print)978-1-59593-689-9
    DOIs
    Publication statusPublished - 2008
    Event35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - San Francisco, United States
    Duration: 7 Jan 200812 Jan 2008
    Conference number: 35

    Conference

    Conference35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    Abbreviated titlePOPL 2008
    CountryUnited States
    CitySan Francisco
    Period7/01/0812/01/08

    Fingerprint Dive into the research topics of 'Enhancing modular OO verification with separation logic'. Together they form a unique fingerprint.

  • Cite this

    Chin, W-N., David, C., Nguyen, H. H., & Qin, S. (2008). Enhancing modular OO verification with separation logic. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008 (pp. 87-99). ACM. https://doi.org/10.1145/1328438.1328452