{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/98295"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/98295","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Testing in learning conjunctive invariants","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.","abstract_html":"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_has_math":false,"creators":["Mahdian, Peyman"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Parthasarathy, Madhusudan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2017,"date_issued":"2017-09-29T17:52:24Z","date_published":"2017-09-29T17:52:24Z","updated_at":"2026-07-22T22:24:35Z","subjects":["Testing","Verification","Loop invariant"],"languages":["en"],"rights":["Copyright 2017 Peyman Mahdian"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/98295","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Parthasarathy, Madhusudan"]},{"key":"dc:creator","label":"Author","values":["Mahdian, Peyman"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2017-09-29T17:52:24Z","2019-09-30T09:15:23Z","2017-07-17","2017-08"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Testing","Verification","Loop invariant"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2017 Peyman Mahdian"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/98295"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2019-08-01","The student, Peyman Mahdian, accepted the attached license on 2017-07-14 at 16:52.","The student, Peyman Mahdian, submitted this Thesis for approval on 2017-07-14 at 17:02.","This Thesis was approved for publication on 2017-07-17 at 10:52.","DSpace SAF Submission Ingestion Package generated from Vireo submission #11479 on 2017-09-29 at 11:19:28","Made available in DSpace on 2017-09-29T17:52:24Z (GMT). No. of bitstreams: 2 MAHDIAN-THESIS-2017.pdf: 350390 bytes, checksum: 6adb724d7d5cabc95d0e67ca669dd3e1 (MD5) LICENSE.txt: 4211 bytes, checksum: 97a7bf219a9a692a7c2762757083ce3d (MD5) Previous issue date: 2017-07-17","Embargo set by: Colleen Fallaw for item 103503 Lift date: 2019-09-29T17:52:45Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Limited Restriction Lifted for Item 103503 on 2019-09-30T09:15:23Z."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Testing in learning conjunctive invariants"]}]}],"canonical_facts":{"dc:contributor":["Parthasarathy, Madhusudan"],"dc:creator":["Mahdian, Peyman"],"dc:date":["2017-09-29T17:52:24Z","2019-09-30T09:15:23Z","2017-07-17","2017-08"],"dc: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.","Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2019-08-01","The student, Peyman Mahdian, accepted the attached license on 2017-07-14 at 16:52.","The student, Peyman Mahdian, submitted this Thesis for approval on 2017-07-14 at 17:02.","This Thesis was approved for publication on 2017-07-17 at 10:52.","DSpace SAF Submission Ingestion Package generated from Vireo submission #11479 on 2017-09-29 at 11:19:28","Made available in DSpace on 2017-09-29T17:52:24Z (GMT). No. of bitstreams: 2 MAHDIAN-THESIS-2017.pdf: 350390 bytes, checksum: 6adb724d7d5cabc95d0e67ca669dd3e1 (MD5) LICENSE.txt: 4211 bytes, checksum: 97a7bf219a9a692a7c2762757083ce3d (MD5) Previous issue date: 2017-07-17","Embargo set by: Colleen Fallaw for item 103503 Lift date: 2019-09-29T17:52:45Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Limited Restriction Lifted for Item 103503 on 2019-09-30T09:15:23Z."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/98295"],"dc:language":["en"],"dc:rights":["Copyright 2017 Peyman Mahdian"],"dc:subject":["Testing","Verification","Loop invariant"],"dc:title":["Testing in learning conjunctive invariants"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:35Z"}