{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/45498"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/45498","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Automatic techniques for proving correctness of heap-manipulating programs","abstract":"Reliability is critical for system software, such as OS kernels, mobile browsers, embedded systems and cloud systems. The correctness of these programs, especially for security, is highly desirable, as they should provide a trustworthy platform for higher-level applications and the end-users. Unfortunately, due to its inherent complexity, the verification process of these programs is typically manual/semi-automatic, tedious, and painful. Automating the reasoning behind these verification tasks and decreasing the dependence on manual help is one of the greatest challenges in software verification. This dissertation presents two logic-based automatic software verification systems, namely Strand and Dryad, that help in the task of verification of heap-manipulating programs, which is one of the most complex aspects of modern software that eludes automatic verification. Strand is a logic that combines an expressive heap-logic with an arbitrary data-logic and admits several powerful decidable fragments. The general decision procedures can be used in not only proving programs correct but also in software analysis and testing. Dryad is a family of logics, including Dryad-tree as a first-order logic for trees and Dryad-sep as a dialect of separation logic. Both the two logics are amenable to automated reasoning using the natural proof strategy, a radically new approach to software verification. Dryad and the natural proof techniques are so far the most efficient logic-based approach that can verify the full correctness of a wide variety of challenging programs, including a large number of programs from various open-source libraries. They hold promise of hatching the next-generation automatic verification techniques.","abstract_html":"Reliability is critical for system software, such as OS kernels, mobile browsers, embedded systems and cloud systems. The correctness of these programs, especially for security, is highly desirable, as they should provide a trustworthy platform for higher-level applications and the end-users. Unfortunately, due to its inherent complexity, the verification process of these programs is typically manual/semi-automatic, tedious, and painful. Automating the reasoning behind these verification tasks and decreasing the dependence on manual help is one of the greatest challenges in software verification. This dissertation presents two logic-based automatic software verification systems, namely Strand and Dryad, that help in the task of verification of heap-manipulating programs, which is one of the most complex aspects of modern software that eludes automatic verification. Strand is a logic that combines an expressive heap-logic with an arbitrary data-logic and admits several powerful decidable fragments. The general decision procedures can be used in not only proving programs correct but also in software analysis and testing. Dryad is a family of logics, including Dryad-tree as a first-order logic for trees and Dryad-sep as a dialect of separation logic. Both the two logics are amenable to automated reasoning using the natural proof strategy, a radically new approach to software verification. Dryad and the natural proof techniques are so far the most efficient logic-based approach that can verify the full correctness of a wide variety of challenging programs, including a large number of programs from various open-source libraries. They hold promise of hatching the next-generation automatic verification techniques.","abstract_has_math":false,"creators":["Qiu, Xiaokang"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Parthasarathy, Madhusudan","Alur, Rajeev","Roşu, Grigore","Viswanathan, Mahesh"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2013,"date_issued":"2013-08-22T16:42:13Z","date_published":"2013-08-22T16:42:13Z","updated_at":"2026-07-22T22:25:36Z","subjects":["separation logic","program verification","heap analysis","Floyd-Hoare Logic","Satisfiability Modulo Theories (SMT) solver","decision procedure","automata","monadic second-order logic","data structure","natural proofs","recursion"],"languages":["en"],"rights":["Copyright 2013 Xiaokang Qiu"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/45498","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Parthasarathy, Madhusudan","Alur, Rajeev","Roşu, Grigore","Viswanathan, Mahesh"]},{"key":"dc:creator","label":"Author","values":["Qiu, Xiaokang"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2013-08-22T16:42:13Z","2013-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":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"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":["separation logic","program verification","heap analysis","Floyd-Hoare Logic","Satisfiability Modulo Theories (SMT) solver","decision procedure","automata","monadic second-order logic","data structure","natural proofs","recursion"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2013 Xiaokang Qiu"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/45498"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Reliability is critical for system software, such as OS kernels, mobile browsers, embedded systems and cloud systems. The correctness of these programs, especially for security, is highly desirable, as they should provide a trustworthy platform for higher-level applications and the end-users. Unfortunately, due to its inherent complexity, the verification process of these programs is typically manual/semi-automatic, tedious, and painful. Automating the reasoning behind these verification tasks and decreasing the dependence on manual help is one of the greatest challenges in software verification. This dissertation presents two logic-based automatic software verification systems, namely Strand and Dryad, that help in the task of verification of heap-manipulating programs, which is one of the most complex aspects of modern software that eludes automatic verification. Strand is a logic that combines an expressive heap-logic with an arbitrary data-logic and admits several powerful decidable fragments. The general decision procedures can be used in not only proving programs correct but also in software analysis and testing. Dryad is a family of logics, including Dryad-tree as a first-order logic for trees and Dryad-sep as a dialect of separation logic. Both the two logics are amenable to automated reasoning using the natural proof strategy, a radically new approach to software verification. Dryad and the natural proof techniques are so far the most efficient logic-based approach that can verify the full correctness of a wide variety of challenging programs, including a large number of programs from various open-source libraries. They hold promise of hatching the next-generation automatic verification techniques.","Item withdrawn by Alexis Thompson (athmpsn1@illinois.edu) on 2013-07-09T17:57:31Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 13 thesisrefs.bib: 55995 bytes, checksum: 83781e0f8e1d043e2313e96e7639b464 (MD5) concl.tex: 4316 bytes, checksum: 19077a13817705fde5850ea644e8960f (MD5) verification.tex: 117248 bytes, checksum: f3fb48a9b3bb4646fc4e3322f2d5d25b (MD5) dryad.tex: 81798 bytes, checksum: 94042c14a91e8f7e01ae50300eedf502 (MD5) natural-proofs.tex: 149516 bytes, checksum: fac69479817150c2e94edf1c86bcc4e4 (MD5) decision-procedures.tex: 88823 bytes, checksum: ad4c9f48996f232047820d5275e788b4 (MD5) strand.tex: 77252 bytes, checksum: 02ed0b2244eb2c68d0364d7cd9b0bd65 (MD5) preliminaries.tex: 11636 bytes, checksum: 863433dc9317bc984a69c249f33f0c55 (MD5) intro.tex: 8983 bytes, checksum: c7974c28d90da22bef8c2e816680050a (MD5) ack.tex: 2097 bytes, checksum: a747ef8a0c24f25ea89508ffd84d0a4b (MD5) abs.tex: 1762 bytes, checksum: 0fbda307238c5f70a871e270d4cc15ff (MD5) main.tex: 81798 bytes, checksum: 94042c14a91e8f7e01ae50300eedf502 (MD5) Qiu_Xiaokang.pdf: 1219686 bytes, checksum: e9bad19f84fe45eb0ab9ede960531e8d (MD5)","Made available in DSpace on 2013-08-22T16:42:13Z (GMT). No. of bitstreams: 14 Xiaokang_Qiu.pdf: 1219686 bytes, checksum: e9bad19f84fe45eb0ab9ede960531e8d (MD5) thesisrefs.bib: 55995 bytes, checksum: 83781e0f8e1d043e2313e96e7639b464 (MD5) concl.tex: 4316 bytes, checksum: 19077a13817705fde5850ea644e8960f (MD5) verification.tex: 117248 bytes, checksum: f3fb48a9b3bb4646fc4e3322f2d5d25b (MD5) dryad.tex: 81798 bytes, checksum: 94042c14a91e8f7e01ae50300eedf502 (MD5) natural-proofs.tex: 149516 bytes, checksum: fac69479817150c2e94edf1c86bcc4e4 (MD5) decision-procedures.tex: 88823 bytes, checksum: ad4c9f48996f232047820d5275e788b4 (MD5) strand.tex: 77252 bytes, checksum: 02ed0b2244eb2c68d0364d7cd9b0bd65 (MD5) preliminaries.tex: 11636 bytes, checksum: 863433dc9317bc984a69c249f33f0c55 (MD5) intro.tex: 8983 bytes, checksum: c7974c28d90da22bef8c2e816680050a (MD5) ack.tex: 2097 bytes, checksum: a747ef8a0c24f25ea89508ffd84d0a4b (MD5) abs.tex: 1762 bytes, checksum: 0fbda307238c5f70a871e270d4cc15ff (MD5) main.tex: 81798 bytes, checksum: 94042c14a91e8f7e01ae50300eedf502 (MD5) license.txt: 4058 bytes, checksum: 7763624ebfe88abf0357060aa3981422 (MD5)"]},{"key":"dc:title","label":"Title","values":["Automatic techniques for proving correctness of heap-manipulating programs"]}]}],"canonical_facts":{"dc:contributor":["Parthasarathy, Madhusudan","Alur, Rajeev","Roşu, Grigore","Viswanathan, Mahesh"],"dc:creator":["Qiu, Xiaokang"],"dc:date":["2013-08-22T16:42:13Z","2013-08"],"dc:description":["Reliability is critical for system software, such as OS kernels, mobile browsers, embedded systems and cloud systems. The correctness of these programs, especially for security, is highly desirable, as they should provide a trustworthy platform for higher-level applications and the end-users. Unfortunately, due to its inherent complexity, the verification process of these programs is typically manual/semi-automatic, tedious, and painful. Automating the reasoning behind these verification tasks and decreasing the dependence on manual help is one of the greatest challenges in software verification. This dissertation presents two logic-based automatic software verification systems, namely Strand and Dryad, that help in the task of verification of heap-manipulating programs, which is one of the most complex aspects of modern software that eludes automatic verification. Strand is a logic that combines an expressive heap-logic with an arbitrary data-logic and admits several powerful decidable fragments. The general decision procedures can be used in not only proving programs correct but also in software analysis and testing. Dryad is a family of logics, including Dryad-tree as a first-order logic for trees and Dryad-sep as a dialect of separation logic. Both the two logics are amenable to automated reasoning using the natural proof strategy, a radically new approach to software verification. Dryad and the natural proof techniques are so far the most efficient logic-based approach that can verify the full correctness of a wide variety of challenging programs, including a large number of programs from various open-source libraries. They hold promise of hatching the next-generation automatic verification techniques.","Item withdrawn by Alexis Thompson (athmpsn1@illinois.edu) on 2013-07-09T17:57:31Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 13 thesisrefs.bib: 55995 bytes, checksum: 83781e0f8e1d043e2313e96e7639b464 (MD5) concl.tex: 4316 bytes, checksum: 19077a13817705fde5850ea644e8960f (MD5) verification.tex: 117248 bytes, checksum: f3fb48a9b3bb4646fc4e3322f2d5d25b (MD5) dryad.tex: 81798 bytes, checksum: 94042c14a91e8f7e01ae50300eedf502 (MD5) natural-proofs.tex: 149516 bytes, checksum: fac69479817150c2e94edf1c86bcc4e4 (MD5) decision-procedures.tex: 88823 bytes, checksum: ad4c9f48996f232047820d5275e788b4 (MD5) strand.tex: 77252 bytes, checksum: 02ed0b2244eb2c68d0364d7cd9b0bd65 (MD5) preliminaries.tex: 11636 bytes, checksum: 863433dc9317bc984a69c249f33f0c55 (MD5) intro.tex: 8983 bytes, checksum: c7974c28d90da22bef8c2e816680050a (MD5) ack.tex: 2097 bytes, checksum: a747ef8a0c24f25ea89508ffd84d0a4b (MD5) abs.tex: 1762 bytes, checksum: 0fbda307238c5f70a871e270d4cc15ff (MD5) main.tex: 81798 bytes, checksum: 94042c14a91e8f7e01ae50300eedf502 (MD5) Qiu_Xiaokang.pdf: 1219686 bytes, checksum: e9bad19f84fe45eb0ab9ede960531e8d (MD5)","Made available in DSpace on 2013-08-22T16:42:13Z (GMT). No. of bitstreams: 14 Xiaokang_Qiu.pdf: 1219686 bytes, checksum: e9bad19f84fe45eb0ab9ede960531e8d (MD5) thesisrefs.bib: 55995 bytes, checksum: 83781e0f8e1d043e2313e96e7639b464 (MD5) concl.tex: 4316 bytes, checksum: 19077a13817705fde5850ea644e8960f (MD5) verification.tex: 117248 bytes, checksum: f3fb48a9b3bb4646fc4e3322f2d5d25b (MD5) dryad.tex: 81798 bytes, checksum: 94042c14a91e8f7e01ae50300eedf502 (MD5) natural-proofs.tex: 149516 bytes, checksum: fac69479817150c2e94edf1c86bcc4e4 (MD5) decision-procedures.tex: 88823 bytes, checksum: ad4c9f48996f232047820d5275e788b4 (MD5) strand.tex: 77252 bytes, checksum: 02ed0b2244eb2c68d0364d7cd9b0bd65 (MD5) preliminaries.tex: 11636 bytes, checksum: 863433dc9317bc984a69c249f33f0c55 (MD5) intro.tex: 8983 bytes, checksum: c7974c28d90da22bef8c2e816680050a (MD5) ack.tex: 2097 bytes, checksum: a747ef8a0c24f25ea89508ffd84d0a4b (MD5) abs.tex: 1762 bytes, checksum: 0fbda307238c5f70a871e270d4cc15ff (MD5) main.tex: 81798 bytes, checksum: 94042c14a91e8f7e01ae50300eedf502 (MD5) license.txt: 4058 bytes, checksum: 7763624ebfe88abf0357060aa3981422 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/45498"],"dc:language":["en"],"dc:rights":["Copyright 2013 Xiaokang Qiu"],"dc:subject":["separation logic","program verification","heap analysis","Floyd-Hoare Logic","Satisfiability Modulo Theories (SMT) solver","decision procedure","automata","monadic second-order logic","data structure","natural proofs","recursion"],"dc:title":["Automatic techniques for proving correctness of heap-manipulating programs"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:36Z"}