Automatic Loop-invariant Generation and Refinement through Selective Sampling

Jiaying Li, Jun Sun, Li Li, Quang Loc Le, Shang-Wei Lin

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

    11 Downloads (Pure)

    Abstract

    Automatic loop-invariant generation is important in program analysis and verification. In this paper, we propose to generate loop-invariants automatically through learning and verification.
    Given a Hoare triple of a program containing a loop, we start with randomly testing the program, collect program states at run-time and categorize them based on whether they satisfy the invariant to be discovered. Next, classification techniques are employed to generate a candidate loop-invariant automatically.
    Afterwards, we refine the candidate through selective sampling so as to overcome the lack of sufficient test cases. Only after a candidate invariant cannot be improved further through selective sampling, we verify whether it can be used to prove the Hoare triple. If it cannot, the generated counterexamples are added as new tests and we repeat the above process. Furthermore, we show
    that by introducing a path-sensitive learning, i.e., partitioning the program states according to program locations they visit and classifying each partition separately, we are able to learn disjunctive loop-invariants. In order to evaluate our idea, a prototype tool has been developed and the experiment results show that our approach complements existing approaches.
    Index Terms—loop-invariant, program verification, classification, active learning, selective sampling
    Original languageEnglish
    Title of host publicationASE 2017
    Subtitle of host publicationProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering
    PublisherIEEE Computer Society
    Pages782-792
    ISBN (Electronic)978-1-5386-2684-9
    Publication statusPublished - 30 Oct 2017
    Event32nd IEEE/ACM International Conference on Automated Software Engineering - Urbana-Champaign, United States
    Duration: 30 Oct 20173 Nov 2017

    Publication series

    NameInternational Conference on Automated Software Engineering
    ISSN (Print)1938-4300

    Conference

    Conference32nd IEEE/ACM International Conference on Automated Software Engineering
    Abbreviated titleASE 2017
    CountryUnited States
    CityUrbana-Champaign
    Period30/10/173/11/17

    Bibliographical note

    © 2017 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. Author can archive post-print for full details see: http://www.ieee.org/publications_standards/publications/rights/rights_policies.html [Accessed: 26/09/2017]

    Fingerprint Dive into the research topics of 'Automatic Loop-invariant Generation and Refinement through Selective Sampling'. Together they form a unique fingerprint.

    Cite this