{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/49385"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/49385","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Specifying and verifying program transformations with PTRANS","abstract":"Software developers, compiler designers, and formal methods researchers all stand to benefit from improved tools for compiler design and verification. Program correctness for compiled languages depends fundamentally on compiler correctness, and compiler optimizations are usually not formally verified due to the effort involved. This is particularly true for optimizations on parallel programs, which are often more difficult to specify correctly and to verify than their sequential counterparts, especially in the presence of relaxed memory models. In this thesis, we outline a Verification Framework for Optimizations and Program Transformations, designed to facilitate stating and reasoning about compiler optimizations and transformations on parallel programs. Most verified compilation projects focus on a single intermediate language and a small number of input and output languages, later adding new targets as extensions; our framework, on the other hand, is designed with language-independence as a first principle, and we seek to generalize and reuse as much as possible across multiple target languages. Our framework makes use of the novel PTRANS transformation specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. The syntax of PTRANS allows cleaner, more proof-amenable specification of program optimizations. PTRANS has two sets of semantics: an abstract semantics for verification, and an executable semantics that allows specifications to act as prototypes for the optimizations themselves, so that candidate optimizations can be tested and refined before going on to formally verify them or include them in a compiler. We address the problems of parallelism head-on by developing a generic framework for memory models in VeriF-OPT, and present a method of importing external analyses such as alias analysis to overcome potential limitations of temporal logic. Finally, we demonstrate the use of the framework by prototyping, testing, and verifying the correctness of several variants of redundant store elimination in two markedly different intermediate languages.","abstract_html":"Software developers, compiler designers, and formal methods researchers all stand to benefit from improved tools for compiler design and verification. Program correctness for compiled languages depends fundamentally on compiler correctness, and compiler optimizations are usually not formally verified due to the effort involved. This is particularly true for optimizations on parallel programs, which are often more difficult to specify correctly and to verify than their sequential counterparts, especially in the presence of relaxed memory models. In this thesis, we outline a Verification Framework for Optimizations and Program Transformations, designed to facilitate stating and reasoning about compiler optimizations and transformations on parallel programs. Most verified compilation projects focus on a single intermediate language and a small number of input and output languages, later adding new targets as extensions; our framework, on the other hand, is designed with language-independence as a first principle, and we seek to generalize and reuse as much as possible across multiple target languages. Our framework makes use of the novel PTRANS transformation specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. The syntax of PTRANS allows cleaner, more proof-amenable specification of program optimizations. PTRANS has two sets of semantics: an abstract semantics for verification, and an executable semantics that allows specifications to act as prototypes for the optimizations themselves, so that candidate optimizations can be tested and refined before going on to formally verify them or include them in a compiler. We address the problems of parallelism head-on by developing a generic framework for memory models in VeriF-OPT, and present a method of importing external analyses such as alias analysis to overcome potential limitations of temporal logic. Finally, we demonstrate the use of the framework by prototyping, testing, and verifying the correctness of several variants of redundant store elimination in two markedly different intermediate languages.","abstract_has_math":false,"creators":["Mansky, William"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Gunter, Elsa L.","Roşu, Grigore","Adve, Vikram S.","Kalvala, Sara"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2014,"date_issued":"2014-05-30T16:41:23Z","date_published":"2014-05-30T16:41:23Z","updated_at":"2026-07-22T22:25:38Z","subjects":["compiler correctness","control flow graphs","temporal logic","rewriting","graph transformation","interactive theorem proving","operational semantics","concurrency","relaxed memory models","Satisfiability Modulo Theories (SMT) solvers"],"languages":["en"],"rights":["Copyright 2014 by William Ernest Mansky"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/49385","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gunter, Elsa L.","Roşu, Grigore","Adve, Vikram S.","Kalvala, Sara"]},{"key":"dc:creator","label":"Author","values":["Mansky, William"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2014-05-30T16:41:23Z","2014-05"]},{"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":["compiler correctness","control flow graphs","temporal logic","rewriting","graph transformation","interactive theorem proving","operational semantics","concurrency","relaxed memory models","Satisfiability Modulo Theories (SMT) solvers"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2014 by William Ernest Mansky"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/49385"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Software developers, compiler designers, and formal methods researchers all stand to benefit from improved tools for compiler design and verification. Program correctness for compiled languages depends fundamentally on compiler correctness, and compiler optimizations are usually not formally verified due to the effort involved. This is particularly true for optimizations on parallel programs, which are often more difficult to specify correctly and to verify than their sequential counterparts, especially in the presence of relaxed memory models. In this thesis, we outline a Verification Framework for Optimizations and Program Transformations, designed to facilitate stating and reasoning about compiler optimizations and transformations on parallel programs. Most verified compilation projects focus on a single intermediate language and a small number of input and output languages, later adding new targets as extensions; our framework, on the other hand, is designed with language-independence as a first principle, and we seek to generalize and reuse as much as possible across multiple target languages. Our framework makes use of the novel PTRANS transformation specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. The syntax of PTRANS allows cleaner, more proof-amenable specification of program optimizations. PTRANS has two sets of semantics: an abstract semantics for verification, and an executable semantics that allows specifications to act as prototypes for the optimizations themselves, so that candidate optimizations can be tested and refined before going on to formally verify them or include them in a compiler. We address the problems of parallelism head-on by developing a generic framework for memory models in VeriF-OPT, and present a method of importing external analyses such as alias analysis to overcome potential limitations of temporal logic. Finally, we demonstrate the use of the framework by prototyping, testing, and verifying the correctness of several variants of redundant store elimination in two markedly different intermediate languages.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2014-04-18T18:48:06Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 36 verif.tex: 53997 bytes, checksum: a98fcad94593fb4696afef44fdc5d5c4 (MD5) uiucthesis2009.cls: 17082 bytes, checksum: 2aaa8503750db3ed51c123468c65fb15 (MD5) starg.png: 5447 bytes, checksum: 1c7de6180ffcbe82588338e40312de06 (MD5) sources.bib: 83024 bytes, checksum: f2f9166d077d96e657e60744564ae172 (MD5) related.tex: 18285 bytes, checksum: 982df8a0e59042adba08b7e0bf15b19c (MD5) ptrans.tex: 41831 bytes, checksum: 7a2f09a14e96bd9a499eba78d733be08 (MD5) pattern.png: 7141 bytes, checksum: 685729d4a6e44db8919940a2164a2c9c (MD5) lock.png: 3942 bytes, checksum: 03d4ff4f95212818e0566615759e2e98 (MD5) intro.tex: 9483 bytes, checksum: c905baf44013594edcb3d006880bd462 (MD5) ils.tex: 59260 bytes, checksum: fd8733f48cb0a9b2830a3e250fa7574f (MD5) exec.tex: 36009 bytes, checksum: f7211d6fd70eeaf17017b5d13ce6f06b (MD5) example2.png: 13208 bytes, checksum: f4fd8e9aaa47006f89fe32d31b9a8756 (MD5) example.png: 6255 bytes, checksum: c8db079f202392a714f91bf78d44c857 (MD5) ex2.png: 32500 bytes, checksum: 4e2609265afce8c27dabaefe97bed533 (MD5) ex1.png: 17199 bytes, checksum: de744747bedb4731aac18d62a769362c (MD5) conc.tex: 23966 bytes, checksum: 917e93ba4962d62124596e557295313d (MD5) abstract.tex: 2180 bytes, checksum: 455e914a3cc996076ecdb0ff70cb9bdc (MD5) thesis.tex: 8292 bytes, checksum: 713cedb58031bc71e1d1fe1ec7da7918 (MD5) trans_syntax.thy: 5069 bytes, checksum: c82b9195820b049cb8cceac6a5faa1b3 (MD5) trans_sim.thy: 41438 bytes, checksum: 4976923166cc1325c79e9193fdaff6f5 (MD5) trans_semantics.thy: 11035 bytes, checksum: a9f07ae4cc40c9400f5881a1190f4f5a (MD5) trans_preds.thy: 19681 bytes, checksum: ad230f0c20fd81f60df10bf71d432533 (MD5) trans_flowgraph.thy: 35519 bytes, checksum: 3dab9f8f6d0aa833a508c71b604c452a (MD5) step_rel.thy: 22265 bytes, checksum: 9e395e56897d5a9aa012821f5a73f5b4 (MD5) memory_model.thy: 23482 bytes, checksum: fb7f3904918351467cdf08895a4f1768 (MD5) LLVM_sim.thy: 11748 bytes, checksum: e25944beeed4a376edd97c33a6c02fbb (MD5) LLVM_RSE_TSO.thy: 26416 bytes, checksum: b2b13cd6e95374f37ddc9fa1462ffa8f (MD5) LLVM_RSE_SC.thy: 17143 bytes, checksum: 0fb91861441f9fc2630c155162c9408f (MD5) LLVM_RSE_PSO.thy: 21761 bytes, checksum: 9d0295c5d36c818fb28347164d21152a (MD5) LLVM_RSE_pre.thy: 4495 bytes, checksum: 51e3cd5c47d0c86c077a3c06323582b3 (MD5) LLVM_preds.thy: 113803 bytes, checksum: 6fea60f832431bd02f7f06a24b3a9a2a (MD5) LLVM.thy: 42540 bytes, checksum: 84b60be2ec123e3fe9df664a244ca185 (MD5) BIL_opt.thy: 17112 bytes, checksum: 6971a4aa3f7be5836e3bc7253ac4fb34 (MD5) BIL_graph.thy: 108205 bytes, checksum: 663e2ed669fbe21e6118d63c625e3c29 (MD5) BIL.thy: 13869 bytes, checksum: 27c538a0bfa362980418424180c3ce8f (MD5) Mansky_William.pdf: 1403686 bytes, checksum: 91579d195897f786bba63a820d5a83b3 (MD5)","Made available in DSpace on 2014-05-30T16:41:23Z (GMT). No. of bitstreams: 37 William_Mansky.pdf: 1403686 bytes, checksum: 91579d195897f786bba63a820d5a83b3 (MD5) trans_syntax.thy: 5069 bytes, checksum: c82b9195820b049cb8cceac6a5faa1b3 (MD5) trans_sim.thy: 41438 bytes, checksum: 4976923166cc1325c79e9193fdaff6f5 (MD5) trans_semantics.thy: 11035 bytes, checksum: a9f07ae4cc40c9400f5881a1190f4f5a (MD5) trans_preds.thy: 19681 bytes, checksum: ad230f0c20fd81f60df10bf71d432533 (MD5) trans_flowgraph.thy: 35519 bytes, checksum: 3dab9f8f6d0aa833a508c71b604c452a (MD5) step_rel.thy: 22265 bytes, checksum: 9e395e56897d5a9aa012821f5a73f5b4 (MD5) memory_model.thy: 23482 bytes, checksum: fb7f3904918351467cdf08895a4f1768 (MD5) LLVM_sim.thy: 11748 bytes, checksum: e25944beeed4a376edd97c33a6c02fbb (MD5) LLVM_RSE_TSO.thy: 26416 bytes, checksum: b2b13cd6e95374f37ddc9fa1462ffa8f (MD5) LLVM_RSE_SC.thy: 17143 bytes, checksum: 0fb91861441f9fc2630c155162c9408f (MD5) LLVM_RSE_PSO.thy: 21761 bytes, checksum: 9d0295c5d36c818fb28347164d21152a (MD5) LLVM_RSE_pre.thy: 4495 bytes, checksum: 51e3cd5c47d0c86c077a3c06323582b3 (MD5) LLVM_preds.thy: 113803 bytes, checksum: 6fea60f832431bd02f7f06a24b3a9a2a (MD5) LLVM.thy: 42540 bytes, checksum: 84b60be2ec123e3fe9df664a244ca185 (MD5) BIL_opt.thy: 17112 bytes, checksum: 6971a4aa3f7be5836e3bc7253ac4fb34 (MD5) BIL_graph.thy: 108205 bytes, checksum: 663e2ed669fbe21e6118d63c625e3c29 (MD5) BIL.thy: 13869 bytes, checksum: 27c538a0bfa362980418424180c3ce8f (MD5) verif.tex: 53997 bytes, checksum: a98fcad94593fb4696afef44fdc5d5c4 (MD5) uiucthesis2009.cls: 17082 bytes, checksum: 2aaa8503750db3ed51c123468c65fb15 (MD5) starg.png: 5447 bytes, checksum: 1c7de6180ffcbe82588338e40312de06 (MD5) sources.bib: 83024 bytes, checksum: f2f9166d077d96e657e60744564ae172 (MD5) related.tex: 18285 bytes, checksum: 982df8a0e59042adba08b7e0bf15b19c (MD5) ptrans.tex: 41831 bytes, checksum: 7a2f09a14e96bd9a499eba78d733be08 (MD5) pattern.png: 7141 bytes, checksum: 685729d4a6e44db8919940a2164a2c9c (MD5) lock.png: 3942 bytes, checksum: 03d4ff4f95212818e0566615759e2e98 (MD5) intro.tex: 9483 bytes, checksum: c905baf44013594edcb3d006880bd462 (MD5) ils.tex: 59260 bytes, checksum: fd8733f48cb0a9b2830a3e250fa7574f (MD5) exec.tex: 36009 bytes, checksum: f7211d6fd70eeaf17017b5d13ce6f06b (MD5) example2.png: 13208 bytes, checksum: f4fd8e9aaa47006f89fe32d31b9a8756 (MD5) example.png: 6255 bytes, checksum: c8db079f202392a714f91bf78d44c857 (MD5) ex2.png: 32500 bytes, checksum: 4e2609265afce8c27dabaefe97bed533 (MD5) ex1.png: 17199 bytes, checksum: de744747bedb4731aac18d62a769362c (MD5) conc.tex: 23966 bytes, checksum: 917e93ba4962d62124596e557295313d (MD5) abstract.tex: 2180 bytes, checksum: 455e914a3cc996076ecdb0ff70cb9bdc (MD5) thesis.tex: 8292 bytes, checksum: 713cedb58031bc71e1d1fe1ec7da7918 (MD5) license.txt: 4063 bytes, checksum: 67fa3bd649000033b53cd525f17e1b12 (MD5)"]},{"key":"dc:title","label":"Title","values":["Specifying and verifying program transformations with PTRANS"]}]}],"canonical_facts":{"dc:contributor":["Gunter, Elsa L.","Roşu, Grigore","Adve, Vikram S.","Kalvala, Sara"],"dc:creator":["Mansky, William"],"dc:date":["2014-05-30T16:41:23Z","2014-05"],"dc:description":["Software developers, compiler designers, and formal methods researchers all stand to benefit from improved tools for compiler design and verification. Program correctness for compiled languages depends fundamentally on compiler correctness, and compiler optimizations are usually not formally verified due to the effort involved. This is particularly true for optimizations on parallel programs, which are often more difficult to specify correctly and to verify than their sequential counterparts, especially in the presence of relaxed memory models. In this thesis, we outline a Verification Framework for Optimizations and Program Transformations, designed to facilitate stating and reasoning about compiler optimizations and transformations on parallel programs. Most verified compilation projects focus on a single intermediate language and a small number of input and output languages, later adding new targets as extensions; our framework, on the other hand, is designed with language-independence as a first principle, and we seek to generalize and reuse as much as possible across multiple target languages. Our framework makes use of the novel PTRANS transformation specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. The syntax of PTRANS allows cleaner, more proof-amenable specification of program optimizations. PTRANS has two sets of semantics: an abstract semantics for verification, and an executable semantics that allows specifications to act as prototypes for the optimizations themselves, so that candidate optimizations can be tested and refined before going on to formally verify them or include them in a compiler. We address the problems of parallelism head-on by developing a generic framework for memory models in VeriF-OPT, and present a method of importing external analyses such as alias analysis to overcome potential limitations of temporal logic. Finally, we demonstrate the use of the framework by prototyping, testing, and verifying the correctness of several variants of redundant store elimination in two markedly different intermediate languages.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2014-04-18T18:48:06Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 36 verif.tex: 53997 bytes, checksum: a98fcad94593fb4696afef44fdc5d5c4 (MD5) uiucthesis2009.cls: 17082 bytes, checksum: 2aaa8503750db3ed51c123468c65fb15 (MD5) starg.png: 5447 bytes, checksum: 1c7de6180ffcbe82588338e40312de06 (MD5) sources.bib: 83024 bytes, checksum: f2f9166d077d96e657e60744564ae172 (MD5) related.tex: 18285 bytes, checksum: 982df8a0e59042adba08b7e0bf15b19c (MD5) ptrans.tex: 41831 bytes, checksum: 7a2f09a14e96bd9a499eba78d733be08 (MD5) pattern.png: 7141 bytes, checksum: 685729d4a6e44db8919940a2164a2c9c (MD5) lock.png: 3942 bytes, checksum: 03d4ff4f95212818e0566615759e2e98 (MD5) intro.tex: 9483 bytes, checksum: c905baf44013594edcb3d006880bd462 (MD5) ils.tex: 59260 bytes, checksum: fd8733f48cb0a9b2830a3e250fa7574f (MD5) exec.tex: 36009 bytes, checksum: f7211d6fd70eeaf17017b5d13ce6f06b (MD5) example2.png: 13208 bytes, checksum: f4fd8e9aaa47006f89fe32d31b9a8756 (MD5) example.png: 6255 bytes, checksum: c8db079f202392a714f91bf78d44c857 (MD5) ex2.png: 32500 bytes, checksum: 4e2609265afce8c27dabaefe97bed533 (MD5) ex1.png: 17199 bytes, checksum: de744747bedb4731aac18d62a769362c (MD5) conc.tex: 23966 bytes, checksum: 917e93ba4962d62124596e557295313d (MD5) abstract.tex: 2180 bytes, checksum: 455e914a3cc996076ecdb0ff70cb9bdc (MD5) thesis.tex: 8292 bytes, checksum: 713cedb58031bc71e1d1fe1ec7da7918 (MD5) trans_syntax.thy: 5069 bytes, checksum: c82b9195820b049cb8cceac6a5faa1b3 (MD5) trans_sim.thy: 41438 bytes, checksum: 4976923166cc1325c79e9193fdaff6f5 (MD5) trans_semantics.thy: 11035 bytes, checksum: a9f07ae4cc40c9400f5881a1190f4f5a (MD5) trans_preds.thy: 19681 bytes, checksum: ad230f0c20fd81f60df10bf71d432533 (MD5) trans_flowgraph.thy: 35519 bytes, checksum: 3dab9f8f6d0aa833a508c71b604c452a (MD5) step_rel.thy: 22265 bytes, checksum: 9e395e56897d5a9aa012821f5a73f5b4 (MD5) memory_model.thy: 23482 bytes, checksum: fb7f3904918351467cdf08895a4f1768 (MD5) LLVM_sim.thy: 11748 bytes, checksum: e25944beeed4a376edd97c33a6c02fbb (MD5) LLVM_RSE_TSO.thy: 26416 bytes, checksum: b2b13cd6e95374f37ddc9fa1462ffa8f (MD5) LLVM_RSE_SC.thy: 17143 bytes, checksum: 0fb91861441f9fc2630c155162c9408f (MD5) LLVM_RSE_PSO.thy: 21761 bytes, checksum: 9d0295c5d36c818fb28347164d21152a (MD5) LLVM_RSE_pre.thy: 4495 bytes, checksum: 51e3cd5c47d0c86c077a3c06323582b3 (MD5) LLVM_preds.thy: 113803 bytes, checksum: 6fea60f832431bd02f7f06a24b3a9a2a (MD5) LLVM.thy: 42540 bytes, checksum: 84b60be2ec123e3fe9df664a244ca185 (MD5) BIL_opt.thy: 17112 bytes, checksum: 6971a4aa3f7be5836e3bc7253ac4fb34 (MD5) BIL_graph.thy: 108205 bytes, checksum: 663e2ed669fbe21e6118d63c625e3c29 (MD5) BIL.thy: 13869 bytes, checksum: 27c538a0bfa362980418424180c3ce8f (MD5) Mansky_William.pdf: 1403686 bytes, checksum: 91579d195897f786bba63a820d5a83b3 (MD5)","Made available in DSpace on 2014-05-30T16:41:23Z (GMT). No. of bitstreams: 37 William_Mansky.pdf: 1403686 bytes, checksum: 91579d195897f786bba63a820d5a83b3 (MD5) trans_syntax.thy: 5069 bytes, checksum: c82b9195820b049cb8cceac6a5faa1b3 (MD5) trans_sim.thy: 41438 bytes, checksum: 4976923166cc1325c79e9193fdaff6f5 (MD5) trans_semantics.thy: 11035 bytes, checksum: a9f07ae4cc40c9400f5881a1190f4f5a (MD5) trans_preds.thy: 19681 bytes, checksum: ad230f0c20fd81f60df10bf71d432533 (MD5) trans_flowgraph.thy: 35519 bytes, checksum: 3dab9f8f6d0aa833a508c71b604c452a (MD5) step_rel.thy: 22265 bytes, checksum: 9e395e56897d5a9aa012821f5a73f5b4 (MD5) memory_model.thy: 23482 bytes, checksum: fb7f3904918351467cdf08895a4f1768 (MD5) LLVM_sim.thy: 11748 bytes, checksum: e25944beeed4a376edd97c33a6c02fbb (MD5) LLVM_RSE_TSO.thy: 26416 bytes, checksum: b2b13cd6e95374f37ddc9fa1462ffa8f (MD5) LLVM_RSE_SC.thy: 17143 bytes, checksum: 0fb91861441f9fc2630c155162c9408f (MD5) LLVM_RSE_PSO.thy: 21761 bytes, checksum: 9d0295c5d36c818fb28347164d21152a (MD5) LLVM_RSE_pre.thy: 4495 bytes, checksum: 51e3cd5c47d0c86c077a3c06323582b3 (MD5) LLVM_preds.thy: 113803 bytes, checksum: 6fea60f832431bd02f7f06a24b3a9a2a (MD5) LLVM.thy: 42540 bytes, checksum: 84b60be2ec123e3fe9df664a244ca185 (MD5) BIL_opt.thy: 17112 bytes, checksum: 6971a4aa3f7be5836e3bc7253ac4fb34 (MD5) BIL_graph.thy: 108205 bytes, checksum: 663e2ed669fbe21e6118d63c625e3c29 (MD5) BIL.thy: 13869 bytes, checksum: 27c538a0bfa362980418424180c3ce8f (MD5) verif.tex: 53997 bytes, checksum: a98fcad94593fb4696afef44fdc5d5c4 (MD5) uiucthesis2009.cls: 17082 bytes, checksum: 2aaa8503750db3ed51c123468c65fb15 (MD5) starg.png: 5447 bytes, checksum: 1c7de6180ffcbe82588338e40312de06 (MD5) sources.bib: 83024 bytes, checksum: f2f9166d077d96e657e60744564ae172 (MD5) related.tex: 18285 bytes, checksum: 982df8a0e59042adba08b7e0bf15b19c (MD5) ptrans.tex: 41831 bytes, checksum: 7a2f09a14e96bd9a499eba78d733be08 (MD5) pattern.png: 7141 bytes, checksum: 685729d4a6e44db8919940a2164a2c9c (MD5) lock.png: 3942 bytes, checksum: 03d4ff4f95212818e0566615759e2e98 (MD5) intro.tex: 9483 bytes, checksum: c905baf44013594edcb3d006880bd462 (MD5) ils.tex: 59260 bytes, checksum: fd8733f48cb0a9b2830a3e250fa7574f (MD5) exec.tex: 36009 bytes, checksum: f7211d6fd70eeaf17017b5d13ce6f06b (MD5) example2.png: 13208 bytes, checksum: f4fd8e9aaa47006f89fe32d31b9a8756 (MD5) example.png: 6255 bytes, checksum: c8db079f202392a714f91bf78d44c857 (MD5) ex2.png: 32500 bytes, checksum: 4e2609265afce8c27dabaefe97bed533 (MD5) ex1.png: 17199 bytes, checksum: de744747bedb4731aac18d62a769362c (MD5) conc.tex: 23966 bytes, checksum: 917e93ba4962d62124596e557295313d (MD5) abstract.tex: 2180 bytes, checksum: 455e914a3cc996076ecdb0ff70cb9bdc (MD5) thesis.tex: 8292 bytes, checksum: 713cedb58031bc71e1d1fe1ec7da7918 (MD5) license.txt: 4063 bytes, checksum: 67fa3bd649000033b53cd525f17e1b12 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/49385"],"dc:language":["en"],"dc:rights":["Copyright 2014 by William Ernest Mansky"],"dc:subject":["compiler correctness","control flow graphs","temporal logic","rewriting","graph transformation","interactive theorem proving","operational semantics","concurrency","relaxed memory models","Satisfiability Modulo Theories (SMT) solvers"],"dc:title":["Specifying and verifying program transformations with PTRANS"],"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:38Z"}