@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 = oct,
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",
note = "IEEE/ACM International Conference on Automated Software Engineering ; Conference date: 01-01-1900",
}