Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
11-2017
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.
Keywords
Interpolation, Loop invariants
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
ASE '17: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering: October 30-November , Urbana-Champaign, IL
First Page
793
Last Page
803
ISBN
9781538626849
Identifier
10.1109/ASE.2017.8115690
Publisher
ACM
City or Country
New York
Citation
LIN, Shang-Wei; SUN, Jun; XIAO, Hao; LIU, Yang; SANA, David; and HANSEN, Henri.
FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers. (2017). ASE '17: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering: October 30-November , Urbana-Champaign, IL. 793-803.
Available at: https://ink.library.smu.edu.sg/sis_research/4713
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/ASE.2017.8115690