Automatic Loop-invariant Generation and Refinement through Selective Sampling

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

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 proceeding › Conference contribution

98 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 language	English
Title of host publication	ASE 2017
Subtitle of host publication	Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering
Publisher	IEEE Computer Society
Pages	782-792
ISBN (Electronic)	978-1-5386-2684-9
Publication status	Published - 30 Oct 2017
Event	32nd IEEE/ACM International Conference on Automated Software Engineering - Urbana-Champaign, United States Duration: 30 Oct 2017 → 3 Nov 2017

Publication series

Name	International Conference on Automated Software Engineering
ISSN (Print)	1938-4300

Conference

Conference	32nd IEEE/ACM International Conference on Automated Software Engineering
Abbreviated title	ASE 2017
Country/Territory	United States
City	Urbana-Champaign
Period	30/10/17 → 3/11/17

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]

Access to Document

Accepted manuscriptAccepted author manuscript, 616 KBLicence: CC BY-NC-ND

https://dl.acm.org/citation.cfm?id=3155562.3155660

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). (International Conference on Automated Software Engineering). IEEE Computer Society. https://dl.acm.org/citation.cfm?id=3155562.3155660

@inproceedings{ebc8a42e9a29426988839ef6819306a1,

title = "Automatic Loop-invariant Generation and Refinement through Selective Sampling",

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",

author = "Jiaying Li and Jun Sun and Li Li and Le, \{Quang Loc\} and Shang-Wei Lin",

note = "{\textcopyright} 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]; 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017 ; Conference date: 30-10-2017 Through 03-11-2017",

year = "2017",

month = oct,

day = "30",

language = "English",

series = "International Conference on Automated Software Engineering",

publisher = "IEEE Computer Society",

pages = "782--792",

booktitle = "ASE 2017",

address = "United States",

}

Li, J, Sun, J, Li, L, Le, QL & 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 . International Conference on Automated Software Engineering, IEEE Computer Society, pp. 782-792, 32nd IEEE/ACM International Conference on Automated Software Engineering, Urbana-Champaign, United States, 30/10/17. <https://dl.acm.org/citation.cfm?id=3155562.3155660>

Automatic Loop-invariant Generation and Refinement through Selective Sampling. / Li, Jiaying; Sun, Jun; Li, Li et al.
ASE 2017: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering . IEEE Computer Society, 2017. p. 782-792 (International Conference on Automated Software Engineering).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Automatic Loop-invariant Generation and Refinement through Selective Sampling

AU - Li, Jiaying

AU - Sun, Jun

AU - Li, Li

AU - Le, Quang Loc

AU - Lin, Shang-Wei

N1 - © 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]

PY - 2017/10/30

Y1 - 2017/10/30

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

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

M3 - Conference contribution

T3 - International Conference on Automated Software Engineering

SP - 782

EP - 792

BT - ASE 2017

PB - IEEE Computer Society

T2 - 32nd IEEE/ACM International Conference on Automated Software Engineering

Y2 - 30 October 2017 through 3 November 2017

ER -

Automatic Loop-invariant Generation and Refinement through Selective Sampling

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Fingerprint

Cite this