{"id":{"repo_id":"nus","oai_identifier":"oai:scholarbank.nus.edu.sg:10635/166280"},"canonical_url":"https://search.dev.ndltd.org/etd/nus/oai:scholarbank.nus.edu.sg:10635/166280","repository":{"repo_id":"nus","name":"National University of Singapore","base_url":"https://scholarbank.nus.edu.sg/oai/request"},"display":{"title":"MECHANIZED VERIFICATION OF GRAPH-MANIPULATING PROGRAMS","abstract":"This thesis tackles the mechanized verification of realistic programs which manipulate heap-represented graphs. We construct a reusable library of formalized graph theory. It is a modular and general library for reasoning about abstract mathematical graphs. We use separation logic to define how such abstract graphs are represented concretely in the heap. To facilitate the spatial entailments involving graphs, we propose an inference rule called Localize which generalize the Ramify rule. We show how this rule can support existential quantifiers in postconditions and smoothly handle modified program variables. To illustrate the generality and power of our techniques, we integrate the mathematical and spatial graph libraries into the Verified Software Toolchain and certify the functional correctness of six graph-manipulating programs written in C. Our proofs are entirely machine-checked in Coq.","abstract_html":"This thesis tackles the mechanized verification of realistic programs which manipulate heap-represented graphs. We construct a reusable library of formalized graph theory. It is a modular and general library for reasoning about abstract mathematical graphs. We use separation logic to define how such abstract graphs are represented concretely in the heap. To facilitate the spatial entailments involving graphs, we propose an inference rule called Localize which generalize the Ramify rule. We show how this rule can support existential quantifiers in postconditions and smoothly handle modified program variables. To illustrate the generality and power of our techniques, we integrate the mathematical and spatial graph libraries into the Verified Software Toolchain and certify the functional correctness of six graph-manipulating programs written in C. Our proofs are entirely machine-checked in Coq.","abstract_has_math":false,"creators":["WANG SHENGYI"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-07-23","date_published":"2019-07-23","updated_at":"2026-07-24T03:32:56Z","subjects":["Verification, Separation logic, Graph-manipulating programs, Coq, CompCert, VST"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":null,"outbound_label":null,"outbound_source":null},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["WANG SHENGYI"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2019-07-23"]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["https://scholarbank.nus.edu.sg/handle/10635/166280"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Verification, Separation logic, Graph-manipulating programs, Coq, CompCert, VST"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://scholarbank.nus.edu.sg/bitstreams/171d9eab-0c69-4a0a-854b-146fba27df3a/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["This thesis tackles the mechanized verification of realistic programs which manipulate heap-represented graphs. We construct a reusable library of formalized graph theory. It is a modular and general library for reasoning about abstract mathematical graphs. We use separation logic to define how such abstract graphs are represented concretely in the heap. To facilitate the spatial entailments involving graphs, we propose an inference rule called Localize which generalize the Ramify rule. We show how this rule can support existential quantifiers in postconditions and smoothly handle modified program variables. To illustrate the generality and power of our techniques, we integrate the mathematical and spatial graph libraries into the Verified Software Toolchain and certify the functional correctness of six graph-manipulating programs written in C. Our proofs are entirely machine-checked in Coq."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["2b44006c8a81b4721110f27fa07ee84b","3b11a89d2113873cdffc821ffeaf707e"]},{"key":"dc:title","label":"Title","values":["MECHANIZED VERIFICATION OF GRAPH-MANIPULATING PROGRAMS"]}]}],"canonical_facts":{"dc:creator":["WANG SHENGYI"],"dc:date.issued":["2019-07-23"],"dc:description.abstract":["This thesis tackles the mechanized verification of realistic programs which manipulate heap-represented graphs. We construct a reusable library of formalized graph theory. It is a modular and general library for reasoning about abstract mathematical graphs. We use separation logic to define how such abstract graphs are represented concretely in the heap. To facilitate the spatial entailments involving graphs, we propose an inference rule called Localize which generalize the Ramify rule. We show how this rule can support existential quantifiers in postconditions and smoothly handle modified program variables. To illustrate the generality and power of our techniques, we integrate the mathematical and spatial graph libraries into the Verified Software Toolchain and certify the functional correctness of six graph-manipulating programs written in C. Our proofs are entirely machine-checked in Coq."],"dc:format.checksum.md5":["2b44006c8a81b4721110f27fa07ee84b","3b11a89d2113873cdffc821ffeaf707e"],"dc:identifier.uri":["https://scholarbank.nus.edu.sg/bitstreams/171d9eab-0c69-4a0a-854b-146fba27df3a/download"],"dc:relation.isreferencedby":["https://scholarbank.nus.edu.sg/handle/10635/166280"],"dc:subject":["Verification, Separation logic, Graph-manipulating programs, Coq, CompCert, VST"],"dc:title":["MECHANIZED VERIFICATION OF GRAPH-MANIPULATING PROGRAMS"],"dc:type":["Thesis"]},"updated_at":"2026-07-24T03:32:56Z"}