{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/92779"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/92779","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Toward language-independent program verification","abstract":"Recent years have seen a renewed interest in the area of deductive program verification, with focus on verifying real-world software components. Success stories include the verification of operating system kernels and of compilers. This dissertation describes techniques for automatically building efficient correct-by-construction program verifiers for real-world languages from operational semantics. In particular, reachability logic is proposed as a foundation for achieving language-independent program verification. Reachability logic can express both operational semantics and program correctness properties, and has a sound and (relatively) complete proof systems that derives the program correctness properties from the operational semantics. These techniques have been implemented in the K verification infrastructure, which in turn yielded automatic program verifiers for C, Java, and JavaScript. These verifiers are evaluated by checking the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). This dissertation also describes the natural proof methodology for automated reasoning about heap properties.","abstract_html":"Recent years have seen a renewed interest in the area of deductive program verification, with focus on verifying real-world software components. Success stories include the verification of operating system kernels and of compilers. This dissertation describes techniques for automatically building efficient correct-by-construction program verifiers for real-world languages from operational semantics. In particular, reachability logic is proposed as a foundation for achieving language-independent program verification. Reachability logic can express both operational semantics and program correctness properties, and has a sound and (relatively) complete proof systems that derives the program correctness properties from the operational semantics. These techniques have been implemented in the K verification infrastructure, which in turn yielded automatic program verifiers for C, Java, and JavaScript. These verifiers are evaluated by checking the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). This dissertation also describes the natural proof methodology for automated reasoning about heap properties.","abstract_has_math":false,"creators":["Ștefănescu, Andrei"],"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","Parthasarathy, Madhusudan","Meseguer, José","Gunter, Elsa","Bjørner, Nikolaj"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2016,"date_issued":"2016-11-10T17:50:16Z","date_published":"2016-11-10T17:50:16Z","updated_at":"2026-07-22T22:26:35Z","subjects":["program verification","operational semantics","automated reasoning","logics","programming languages"],"languages":["en"],"rights":["Copyright 2016 Andrei Stefanescu"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/92779","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Roșu, Grigore","Parthasarathy, Madhusudan","Meseguer, José","Gunter, Elsa","Bjørner, Nikolaj"]},{"key":"dc:creator","label":"Author","values":["Ștefănescu, Andrei"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2016-11-10T17:50:16Z","2016-07-08","2016-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":["program verification","operational semantics","automated reasoning","logics","programming languages"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2016 Andrei Stefanescu"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/92779"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Recent years have seen a renewed interest in the area of deductive program verification, with focus on verifying real-world software components. Success stories include the verification of operating system kernels and of compilers. This dissertation describes techniques for automatically building efficient correct-by-construction program verifiers for real-world languages from operational semantics. In particular, reachability logic is proposed as a foundation for achieving language-independent program verification. Reachability logic can express both operational semantics and program correctness properties, and has a sound and (relatively) complete proof systems that derives the program correctness properties from the operational semantics. These techniques have been implemented in the K verification infrastructure, which in turn yielded automatic program verifiers for C, Java, and JavaScript. These verifiers are evaluated by checking the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). This dissertation also describes the natural proof methodology for automated reasoning about heap properties.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-11-09 without embargo terms","The student, Andrei Ștefănescu, accepted the attached license on 2016-07-08 at 11:59.","The student, Andrei Ștefănescu, submitted this Dissertation for approval on 2016-07-08 at 12:13.","This Dissertation was approved for publication on 2016-07-08 at 14:42.","DSpace SAF Submission Ingestion Package generated from Vireo submission #9821 on 2016-11-09 at 10:23:07","Made available in DSpace on 2016-11-10T17:50:16Z (GMT). No. of bitstreams: 3 STEFANESCU-DISSERTATION-2016.pdf: 1708711 bytes, checksum: 3243b67051ae21634b5a449c4715aa99 (MD5) LICENSE.txt: 4214 bytes, checksum: 4c6592a9434fd2824681df24acc9d583 (MD5) PROQUEST_LICENSE.txt: 4560 bytes, checksum: c08caba6f776b5e385952c1d9600ac02 (MD5) Previous issue date: 2016-07-08"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Toward language-independent program verification"]}]}],"canonical_facts":{"dc:contributor":["Roșu, Grigore","Parthasarathy, Madhusudan","Meseguer, José","Gunter, Elsa","Bjørner, Nikolaj"],"dc:creator":["Ștefănescu, Andrei"],"dc:date":["2016-11-10T17:50:16Z","2016-07-08","2016-08"],"dc:description":["Recent years have seen a renewed interest in the area of deductive program verification, with focus on verifying real-world software components. Success stories include the verification of operating system kernels and of compilers. This dissertation describes techniques for automatically building efficient correct-by-construction program verifiers for real-world languages from operational semantics. In particular, reachability logic is proposed as a foundation for achieving language-independent program verification. Reachability logic can express both operational semantics and program correctness properties, and has a sound and (relatively) complete proof systems that derives the program correctness properties from the operational semantics. These techniques have been implemented in the K verification infrastructure, which in turn yielded automatic program verifiers for C, Java, and JavaScript. These verifiers are evaluated by checking the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). This dissertation also describes the natural proof methodology for automated reasoning about heap properties.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-11-09 without embargo terms","The student, Andrei Ștefănescu, accepted the attached license on 2016-07-08 at 11:59.","The student, Andrei Ștefănescu, submitted this Dissertation for approval on 2016-07-08 at 12:13.","This Dissertation was approved for publication on 2016-07-08 at 14:42.","DSpace SAF Submission Ingestion Package generated from Vireo submission #9821 on 2016-11-09 at 10:23:07","Made available in DSpace on 2016-11-10T17:50:16Z (GMT). No. of bitstreams: 3 STEFANESCU-DISSERTATION-2016.pdf: 1708711 bytes, checksum: 3243b67051ae21634b5a449c4715aa99 (MD5) LICENSE.txt: 4214 bytes, checksum: 4c6592a9434fd2824681df24acc9d583 (MD5) PROQUEST_LICENSE.txt: 4560 bytes, checksum: c08caba6f776b5e385952c1d9600ac02 (MD5) Previous issue date: 2016-07-08"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/92779"],"dc:language":["en"],"dc:rights":["Copyright 2016 Andrei Stefanescu"],"dc:subject":["program verification","operational semantics","automated reasoning","logics","programming languages"],"dc:title":["Toward language-independent 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:26:35Z"}