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

• Main Authors: LIN, Shang-Wei, SUN, Jun, XIAO, Hao, LIU, Yang, SANA, David, HANSEN, Henri
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2017
• Subjects: Interpolation; Loop invariants; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4713; https://ink.library.smu.edu.sg/context/sis_research/article/5716/viewcontent/FiB_pv.pdf
• Institution: Singapore Management University

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