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

    Tutkimustuotos: KonferenssiartikkeliScientificvertaisarvioitu

    5 Sitaatiot (Scopus)

    Abstrakti

    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.
    AlkuperäiskieliEnglanti
    OtsikkoProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering
    AlaotsikkoASE 2017
    ToimittajatGrigore Rosu, Massimiliano Di Penta, Tien N. Nguyen
    KustantajaIEEE Press
    Sivut793-803
    Sivumäärä11
    ISBN (elektroninen)978-1-5386-2684-9
    DOI - pysyväislinkit
    TilaJulkaistu - lokak. 2017
    OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisussa
    TapahtumaIEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING -
    Kesto: 1 tammik. 1900 → …

    Julkaisusarja

    NimiIEEE/ACM International Conference on Automated Software Engineering
    KustantajaIEEE
    ISSN (painettu)1938-4300

    Conference

    ConferenceIEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING
    Ajanjakso1/01/00 → …

    Julkaisufoorumi-taso

    • Jufo-taso 2

    Sormenjälki

    Sukella tutkimusaiheisiin 'FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

    Siteeraa tätä