ASE 2017

2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017), October 30 – November 3, 2017, Urbana-Champaign, IL, USA

Desktop Layout

Program Synthesis
Technical Research
FiB: Squeezing Loop Invariants by Interpolation between Forward/Backward Predicate Transformers
Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sanán, and Henri Hansen
(Nanyang Technological University, Singapore; Singapore University of Technology and Design, Singapore; Tampere University of Technology, Finland)
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.

Authors:


Time stamp: 2019-06-19T15:05:47+02:00