Testing in learning conjunctive invariants
type: CreativeWork
description: 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.
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.
author: Mahdian, Peyman
language: en
keywords: Testing, Verification, Loop invariant
date published: 2017-09-29T17:52:24Z
date modified: 2026-07-22T22:24:35Z
provider: University of Illinois - Urbana-Champaign
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: University of Illinois at Urbana-Champaign

PropertyValue
property ID: Handle
value: http://hdl.handle.net/2142/98295