{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/104795"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/104795","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Semantics-based program verification","abstract":"\"We present language-independent formal methods that are parameterized by the operational semantics of languages. We provide the theory, implementation, and extensive evaluation of the language-parametric formal methods. Specifically, we consider two formal analyses: program verification and program equivalence. First, we propose a novel notion of bisimulation, which we call cut-bisimulation, allowing the two programs to semantically synchronize at relevant \"\"cut\"\" points, but to evolve independently otherwise. Employing the cut-bisimulation, we develop a language-independent equivalence checking algorithm, parameterized by the input and output language semantics, to prove equivalence of programs written in possibly different languages. We implement the algorithm in the K framework, yielding the first language-parametric program equivalence checker. To demonstrate the practical feasibility of the language-parametric formal methods, we instantiate a language-independent deductive program verifier by plugging-in four real-world language semantics, C, Java, JavaScript, and Ethereum Virtual Machine (EVM), and use them to verify full functional correctness of challenging heap-manipulating programs and high-profile commercial smart contracts. In particular, to the best of our knowledge, the JavaScript and EVM verifiers are the first deductive program verifier for these languages.\"","abstract_html":""We present language-independent formal methods that are parameterized by the operational semantics of languages. We provide the theory, implementation, and extensive evaluation of the language-parametric formal methods. Specifically, we consider two formal analyses: program verification and program equivalence. First, we propose a novel notion of bisimulation, which we call cut-bisimulation, allowing the two programs to semantically synchronize at relevant ""cut"" points, but to evolve independently otherwise. Employing the cut-bisimulation, we develop a language-independent equivalence checking algorithm, parameterized by the input and output language semantics, to prove equivalence of programs written in possibly different languages. We implement the algorithm in the K framework, yielding the first language-parametric program equivalence checker. To demonstrate the practical feasibility of the language-parametric formal methods, we instantiate a language-independent deductive program verifier by plugging-in four real-world language semantics, C, Java, JavaScript, and Ethereum Virtual Machine (EVM), and use them to verify full functional correctness of challenging heap-manipulating programs and high-profile commercial smart contracts. In particular, to the best of our knowledge, the JavaScript and EVM verifiers are the first deductive program verifier for these languages."","abstract_has_math":false,"creators":["Park, Daejun"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Roşu, Grigore","Adve, Vikram","Miller, Andrew","Bjørner, Nikolaj"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-08-23T19:51:44Z","date_published":"2019-08-23T19:51:44Z","updated_at":"2026-07-22T22:24:42Z","subjects":["Program verification","Program equivalence"],"languages":["en"],"rights":["Copyright 2019 Daejun Park"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/104795","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Roşu, Grigore","Adve, Vikram","Miller, Andrew","Bjørner, Nikolaj"]},{"key":"dc:creator","label":"Author","values":["Park, Daejun"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2019-08-23T19:51:44Z","2019-04-09","2019-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":["Program verification","Program equivalence"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2019 Daejun Park"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/104795"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["\"We present language-independent formal methods that are parameterized by the operational semantics of languages. We provide the theory, implementation, and extensive evaluation of the language-parametric formal methods. Specifically, we consider two formal analyses: program verification and program equivalence. First, we propose a novel notion of bisimulation, which we call cut-bisimulation, allowing the two programs to semantically synchronize at relevant \"\"cut\"\" points, but to evolve independently otherwise. Employing the cut-bisimulation, we develop a language-independent equivalence checking algorithm, parameterized by the input and output language semantics, to prove equivalence of programs written in possibly different languages. We implement the algorithm in the K framework, yielding the first language-parametric program equivalence checker. To demonstrate the practical feasibility of the language-parametric formal methods, we instantiate a language-independent deductive program verifier by plugging-in four real-world language semantics, C, Java, JavaScript, and Ethereum Virtual Machine (EVM), and use them to verify full functional correctness of challenging heap-manipulating programs and high-profile commercial smart contracts. In particular, to the best of our knowledge, the JavaScript and EVM verifiers are the first deductive program verifier for these languages.\"","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-08-22 without embargo terms","The student, Daejun Park, accepted the attached license on 2019-04-08 at 23:27.","The student, Daejun Park, submitted this Dissertation for approval on 2019-04-08 at 23:32.","This Dissertation was approved for publication on 2019-04-09 at 09:29.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13528 on 2019-08-22 at 14:42:21","Made available in DSpace on 2019-08-23T19:51:44Z (GMT). No. of bitstreams: 2 PARK-DISSERTATION-2019.pdf: 1191120 bytes, checksum: 7af3f4a7c8d39554c05f9452fb11a000 (MD5) LICENSE.txt: 4208 bytes, checksum: 66de8493a06d73172fa93f89c996c92b (MD5) Previous issue date: 2019-04-09"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Semantics-based program verification"]}]}],"canonical_facts":{"dc:contributor":["Roşu, Grigore","Adve, Vikram","Miller, Andrew","Bjørner, Nikolaj"],"dc:creator":["Park, Daejun"],"dc:date":["2019-08-23T19:51:44Z","2019-04-09","2019-05"],"dc:description":["\"We present language-independent formal methods that are parameterized by the operational semantics of languages. We provide the theory, implementation, and extensive evaluation of the language-parametric formal methods. Specifically, we consider two formal analyses: program verification and program equivalence. First, we propose a novel notion of bisimulation, which we call cut-bisimulation, allowing the two programs to semantically synchronize at relevant \"\"cut\"\" points, but to evolve independently otherwise. Employing the cut-bisimulation, we develop a language-independent equivalence checking algorithm, parameterized by the input and output language semantics, to prove equivalence of programs written in possibly different languages. We implement the algorithm in the K framework, yielding the first language-parametric program equivalence checker. To demonstrate the practical feasibility of the language-parametric formal methods, we instantiate a language-independent deductive program verifier by plugging-in four real-world language semantics, C, Java, JavaScript, and Ethereum Virtual Machine (EVM), and use them to verify full functional correctness of challenging heap-manipulating programs and high-profile commercial smart contracts. In particular, to the best of our knowledge, the JavaScript and EVM verifiers are the first deductive program verifier for these languages.\"","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-08-22 without embargo terms","The student, Daejun Park, accepted the attached license on 2019-04-08 at 23:27.","The student, Daejun Park, submitted this Dissertation for approval on 2019-04-08 at 23:32.","This Dissertation was approved for publication on 2019-04-09 at 09:29.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13528 on 2019-08-22 at 14:42:21","Made available in DSpace on 2019-08-23T19:51:44Z (GMT). No. of bitstreams: 2 PARK-DISSERTATION-2019.pdf: 1191120 bytes, checksum: 7af3f4a7c8d39554c05f9452fb11a000 (MD5) LICENSE.txt: 4208 bytes, checksum: 66de8493a06d73172fa93f89c996c92b (MD5) Previous issue date: 2019-04-09"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/104795"],"dc:language":["en"],"dc:rights":["Copyright 2019 Daejun Park"],"dc:subject":["Program verification","Program equivalence"],"dc:title":["Semantics-based program verification"],"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:24:42Z"}