FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers

Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sanán, Henri Hansen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

    5 Citations (Scopus)

    Abstract

    Loop invariant generation is a fundamental problem in program analysis and verification. In this work, we propose a new approach to automatically constructing inductive loop invariants. The key idea is to aggressively squeeze an inductive invariant based on Craig interpolants between forward and backward reachability analysis. We have evaluated our approach by a set of loop benchmarks, and experimental results show that our approach is promising.
    Original languageEnglish
    Title of host publicationProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering
    Subtitle of host publicationASE 2017
    EditorsGrigore Rosu, Massimiliano Di Penta, Tien N. Nguyen
    PublisherIEEE Press
    Pages793-803
    Number of pages11
    ISBN (Electronic)978-1-5386-2684-9
    DOIs
    Publication statusPublished - Oct 2017
    Publication typeA4 Article in a conference publication
    EventIEEE/ACM International Conference on Automated Software Engineering -
    Duration: 1 Jan 1900 → …

    Publication series

    NameIEEE/ACM International Conference on Automated Software Engineering
    PublisherIEEE
    ISSN (Print)1938-4300

    Conference

    ConferenceIEEE/ACM International Conference on Automated Software Engineering
    Period1/01/00 → …

    Publication forum classification

    • Publication forum level 2

    Fingerprint

    Dive into the research topics of 'FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers'. Together they form a unique fingerprint.

    Cite this