Loop Invariant Synthesis in a Combined Domain

Shengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin

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

    Abstract

    Automated verification of memory safety and functional correctness for heap-manipulating programs has been a challenging task, especially when dealing with complex data structures with strong invariants involving both shape and numerical properties. Existing verification systems usually rely on users to supply annotations, which can be tedious and error-prone and can significantly restrict the scalability of the verification system. In this paper, we reduce the need of user annotations by automatically inferring loop invariants over an abstract domain with both separation and numerical information. Our loop invariant synthesis is conducted automatically by a fixpoint iteration process, equipped with newly designed abstraction mechanism, and join and widening operators. Initial experiments have confirmed that we can synthesise loop invariants with non-trivial constraints.
    Original languageEnglish
    Title of host publicationFormal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings
    PublisherSpringer Berlin
    Pages468-484
    ISBN (Electronic)9783642169014
    ISBN (Print)9783642169007
    DOIs
    Publication statusPublished - 2010
    EventFormal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods - Shanghai, China
    Duration: 17 Nov 201019 Nov 2010
    Conference number: 12

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer

    Conference

    ConferenceFormal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods
    Abbreviated titleICFEM 2010
    CountryChina
    CityShanghai
    Period17/11/1019/11/10

    Fingerprint Dive into the research topics of 'Loop Invariant Synthesis in a Combined Domain'. Together they form a unique fingerprint.

  • Cite this

    Qin, S., He, G., Luo, C., & Chin, W-N. (2010). Loop Invariant Synthesis in a Combined Domain. In Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings (pp. 468-484). (Lecture Notes in Computer Science ). Springer Berlin. https://doi.org/10.1007/978-3-642-16901-4_31