TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

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

Tutkimustuotosvertaisarvioitu

Yksityiskohdat

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 - lokakuuta 2017
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisussa
TapahtumaIEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING -
Kesto: 1 tammikuuta 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 → …

Tiivistelmä

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.

Julkaisufoorumi-taso