Files in this item



application/pdfMAHDIAN-THESIS-2017.pdf (350kB)
(no description provided)PDF


Title:Testing in learning conjunctive invariants
Author(s):Mahdian, Peyman
Advisor(s):Parthasarathy, Madhusudan
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Loop invariant
Abstract: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.
Issue Date:2017-07-17
Rights Information:Copyright 2017 Peyman Mahdian
Date Available in IDEALS:2017-09-29
Date Deposited:2017-08

This item appears in the following Collection(s)

Item Statistics