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

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

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

Full description

Saved in:
Bibliographic Details
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
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
Description
Summary: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.

Similar Items