Files in this item
Files | Description | Format |
---|---|---|
application/pdf ![]() | (no description provided) |
Description
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 |
Degree: | M.S. |
Genre: | Thesis |
Subject(s): | Testing
Verification 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 |
Type: | Text |
URI: | http://hdl.handle.net/2142/98295 |
Rights Information: | Copyright 2017 Peyman Mahdian |
Date Available in IDEALS: | 2017-09-29 2019-09-30 |
Date Deposited: | 2017-08 |
This item appears in the following Collection(s)
-
Dissertations and Theses - Computer Science
Dissertations and Theses from the Dept. of Computer Science -
Graduate Dissertations and Theses at Illinois
Graduate Theses and Dissertations at Illinois