Automatic Loop-invariant Generation and Refinement through Selective Sampling

Jiaying Li, Jun Sun, Li Li, Quang Loc Le, Shang-Wei Lin

Research output: Chapter in Book/Report/Conference proceedingChapter

5 Downloads (Pure)

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.
Index Terms—loop-invariant, program verification, classification, active learning, selective sampling
Original languageEnglish
Title of host publicationASE 2017
Subtitle of host publicationProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering
PublisherIEEE Computer Society
Pages782-792
ISBN (Electronic)978-1-5386-2684-9
Publication statusPublished - 30 Oct 2017
Event32nd IEEE/ACM International Conference on Automated Software Engineering - Urbana-Champaign, United States
Duration: 30 Oct 20173 Nov 2017

Conference

Conference32nd IEEE/ACM International Conference on Automated Software Engineering
Abbreviated titleASE 2017
CountryUnited States
CityUrbana-Champaign
Period30/10/173/11/17

    Fingerprint

Bibliographical note

© 2017 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. Author can archive post-print for full details see: http://www.ieee.org/publications_standards/publications/rights/rights_policies.html [Accessed: 26/09/2017]

Cite this

Li, J., Sun, J., Li, L., Le, Q. L., & Lin, S-W. (2017). Automatic Loop-invariant Generation and Refinement through Selective Sampling. In ASE 2017: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering (pp. 782-792). IEEE Computer Society.