Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

11-2017

Abstract

Automatic loop-invariant generation is important in program analysis and verification. In this paper, we propose to generate loop-invariants automatically through learning and verification. Given a Hoare triple of a program containing a loop, we start with randomly testing the program, collect program states at run-time and categorize them based on whether they satisfy the invariant to be discovered. Next, classification techniques are employed to generate a candidate loop-invariant automatically. Afterwards, we refine the candidate through selective sampling so as to overcome the lack of sufficient test cases. Only after a candidate invariant cannot be improved further through selective sampling, we verify whether it can be used to prove the Hoare triple. If it cannot, the generated counterexamples are added as new tests and we repeat the above process. Furthermore, we show that by introducing a path-sensitive learning, i.e., partitioning the program states according to program locations they visit and classifying each partition separately, we are able to learn disjunctive loop-invariants. In order to evaluate our idea, a prototype tool has been developed and the experiment results show that our approach complements existing approaches.

Keywords

Active learning, classification, Loop-invariant, program verification, selective sampling

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 3, Urbana-Champaign, IL

First Page

782

Last Page

792

ISBN

9781538626849

Identifier

10.1109/ASE.2017.8115689

Publisher

ACM

City or Country

New York

Additional URL

https://doi.org/10.1109/ASE.2017.8115689

Download

Share

COinS