TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

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

Tutkimustuotosvertaisarvioitu

Standard

FiB : Squeezing loop invariants by interpolation between forward/backward predicate transformers. / Lin, Shang-Wei; Sun, Jun; Xiao, Hao; Liu, Yang; Sanán, David; Hansen, Henri.

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering: ASE 2017. toim. / Grigore Rosu; Massimiliano Di Penta; Tien N. Nguyen. IEEE Press, 2017. s. 793-803 (IEEE/ACM International Conference on Automated Software Engineering).

Tutkimustuotosvertaisarvioitu

Harvard

Lin, S-W, Sun, J, Xiao, H, Liu, Y, Sanán, D & Hansen, H 2017, FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers. julkaisussa G Rosu, M Di Penta & TN Nguyen (toim), Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering: ASE 2017. IEEE/ACM International Conference on Automated Software Engineering, IEEE Press, Sivut 793-803, IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, 1/01/00. https://doi.org/10.1109/ASE.2017.8115690

APA

Lin, S-W., Sun, J., Xiao, H., Liu, Y., Sanán, D., & Hansen, H. (2017). FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers. teoksessa G. Rosu, M. Di Penta, & T. N. Nguyen (Toimittajat), Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering: ASE 2017 (Sivut 793-803). (IEEE/ACM International Conference on Automated Software Engineering). IEEE Press. https://doi.org/10.1109/ASE.2017.8115690

Vancouver

Lin S-W, Sun J, Xiao H, Liu Y, Sanán D, Hansen H. FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers. julkaisussa Rosu G, Di Penta M, Nguyen TN, toimittajat, Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering: ASE 2017. IEEE Press. 2017. s. 793-803. (IEEE/ACM International Conference on Automated Software Engineering). https://doi.org/10.1109/ASE.2017.8115690

Author

Lin, Shang-Wei ; Sun, Jun ; Xiao, Hao ; Liu, Yang ; Sanán, David ; Hansen, Henri. / FiB : Squeezing loop invariants by interpolation between forward/backward predicate transformers. Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering: ASE 2017. Toimittaja / Grigore Rosu ; Massimiliano Di Penta ; Tien N. Nguyen. IEEE Press, 2017. Sivut 793-803 (IEEE/ACM International Conference on Automated Software Engineering).

Bibtex - Lataa

@inproceedings{79a4df10014744d89e50d7e12e574f28,
title = "FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers",
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.",
author = "Shang-Wei Lin and Jun Sun and Hao Xiao and Yang Liu and David San{\'a}n and Henri Hansen",
year = "2017",
month = "10",
doi = "10.1109/ASE.2017.8115690",
language = "English",
series = "IEEE/ACM International Conference on Automated Software Engineering",
publisher = "IEEE Press",
pages = "793--803",
editor = "Grigore Rosu and {Di Penta}, Massimiliano and Nguyen, {Tien N.}",
booktitle = "Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering",

}

RIS (suitable for import to EndNote) - Lataa

TY - GEN

T1 - FiB

T2 - Squeezing loop invariants by interpolation between forward/backward predicate transformers

AU - Lin, Shang-Wei

AU - Sun, Jun

AU - Xiao, Hao

AU - Liu, Yang

AU - Sanán, David

AU - Hansen, Henri

PY - 2017/10

Y1 - 2017/10

N2 - 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.

AB - 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.

U2 - 10.1109/ASE.2017.8115690

DO - 10.1109/ASE.2017.8115690

M3 - Conference contribution

T3 - IEEE/ACM International Conference on Automated Software Engineering

SP - 793

EP - 803

BT - Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering

A2 - Rosu, Grigore

A2 - Di Penta, Massimiliano

A2 - Nguyen, Tien N.

PB - IEEE Press

ER -