Automatic loop-invariant generation and refinement through selective sampling

• Main Authors: LI, Jiaying, SUN, Jun, LI, Li, LE, Quang Loc, LIN, Shang-Wei
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2017
• Subjects: Active learning; classification; Loop-invariant; program verification; selective sampling; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4712; https://ink.library.smu.edu.sg/context/sis_research/article/5715/viewcontent/Automatic_loop_variant_ase17_av.pdf
• Institution: Singapore Management University

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