Testing in learning conjunctive invariants

We show a new approach in learning conjunctive invariants using dynamic testing of the program. Coming up with correct set of loop invariant is the most challenging part of any verification methods. Although new methods tend to generate a large number of possible invariants hoping this set contains all required invariants needed to verify the program, this large number will cause a significant delay in verification which often ends up to a time out. Our approach introduce a new method in which we can solve this problem by reducing the number of generated candidate invariants. We apply our method in a verification engine that uses natural proofs for heap verification. We implement our method by running tests for linked list data structures and evaluate it by comparing the results to the original approach without testing. We also use an existing GPU verification tool, called GPUVerify, and apply our method to it. Finally, we show that our approach can significantly improve the verification time and in some cases prove programs that were initially timed out.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2017

Author dc:creator

• Mahdian, Peyman

Contributors dc:contributor

• Parthasarathy, Madhusudan

• Testing
• Verification
• Loop invariant

Statement dc:rights

• Copyright 2017 Peyman Mahdian

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/98295

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/98295