{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/127268"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/127268","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Automated reasoning for fixpoints and concrete execution in matching logic","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","abstract_has_math":false,"creators":["Rodrigues, Nishant Joseph"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Rosu, Grigore","Meseguer, Jose","Escobar, Santiago","Zhang, Lingming"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-12-05","date_published":"2024-12-05","updated_at":"2026-07-22T22:25:03Z","subjects":["Fixpoint","Matching Logic","Logic","Automata"],"languages":["en","eng"],"rights":["Copyright Nishant Rodrigues 2024"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/127268","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Rosu, Grigore","Meseguer, Jose","Escobar, Santiago","Zhang, Lingming"]},{"key":"dc:creator","label":"Author","values":["Rodrigues, Nishant Joseph"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-12-05","2024-12"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"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":["Fixpoint","Matching Logic","Logic","Automata"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright Nishant Rodrigues 2024"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/127268"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","The student, Nishant Rodrigues, accepted the attached license on 2024-12-04 at 12:03.","The student, Nishant Rodrigues, submitted this Dissertation for approval on 2024-12-04 at 12:14.","This Dissertation was approved for publication on 2024-12-05 at 16:18.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21497 on 2025-03-28 at 14:28:03","The K Framework takes the semantics-first approach to programming language development. This involves building a mathematical formalization of a programming language, and automatically deriving varied language tools from it. This methodology has proved efficient and practical for real-world programming language development. Further evidence of this is given in this work, in the development of formal semantics for the Ethereum Virtual Machine and the Boogie IVL. Getting here has meant developing complex algorithms, to both enable the high level of abstraction needed for complex language development as well as to produce a performant implementation as expected of language tools. The flip side of this complexity is that it makes it difficult to trust in K's correctness. To remedy this, we seek to produce formal proofs alongside each run of K's tools, leveraging K's mathematical foundations in matching logic. This work focuses on capturing two aspects of this in matching logic---fixpoint reasoning, and producing proofs for concrete execution. Fixpoint reasoning is core to many of K's tools; used for example in the definition of abstract data types, and in deductive verification via reachability logic. Using matching logic, we develop a small set of proof-rules amenable to automation, and demonstrate their use in a variety of domains, including linear temporal logic, separation logic, reachability logic, and regular languages. Of particular interest is that we are able to capture computational models as a \\emph{structurally-analogous} logical formula. This gives us the ability to logically manipulate the computational structure, making it almost trivial to extract proofs from decision procedures that operate over them. We capture proofs of equivalence between regular expressions by extracting such proofs from Brzozowski's method that manipulates finite automata. For the second aspect, concrete execution, we build on previous work to produce efficient, compact proofs for concrete execution. Our key contributions are the development of an efficient proof format, and generation of proofs in a streaming fashion. This enables proofs for long running executions."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Automated reasoning for fixpoints and concrete execution in matching logic"]}]}],"canonical_facts":{"dc:contributor":["Rosu, Grigore","Meseguer, Jose","Escobar, Santiago","Zhang, Lingming"],"dc:creator":["Rodrigues, Nishant Joseph"],"dc:date":["2024-12-05","2024-12"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms","The student, Nishant Rodrigues, accepted the attached license on 2024-12-04 at 12:03.","The student, Nishant Rodrigues, submitted this Dissertation for approval on 2024-12-04 at 12:14.","This Dissertation was approved for publication on 2024-12-05 at 16:18.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21497 on 2025-03-28 at 14:28:03","The K Framework takes the semantics-first approach to programming language development. This involves building a mathematical formalization of a programming language, and automatically deriving varied language tools from it. This methodology has proved efficient and practical for real-world programming language development. Further evidence of this is given in this work, in the development of formal semantics for the Ethereum Virtual Machine and the Boogie IVL. Getting here has meant developing complex algorithms, to both enable the high level of abstraction needed for complex language development as well as to produce a performant implementation as expected of language tools. The flip side of this complexity is that it makes it difficult to trust in K's correctness. To remedy this, we seek to produce formal proofs alongside each run of K's tools, leveraging K's mathematical foundations in matching logic. This work focuses on capturing two aspects of this in matching logic---fixpoint reasoning, and producing proofs for concrete execution. Fixpoint reasoning is core to many of K's tools; used for example in the definition of abstract data types, and in deductive verification via reachability logic. Using matching logic, we develop a small set of proof-rules amenable to automation, and demonstrate their use in a variety of domains, including linear temporal logic, separation logic, reachability logic, and regular languages. Of particular interest is that we are able to capture computational models as a \\emph{structurally-analogous} logical formula. This gives us the ability to logically manipulate the computational structure, making it almost trivial to extract proofs from decision procedures that operate over them. We capture proofs of equivalence between regular expressions by extracting such proofs from Brzozowski's method that manipulates finite automata. For the second aspect, concrete execution, we build on previous work to produce efficient, compact proofs for concrete execution. Our key contributions are the development of an efficient proof format, and generation of proofs in a streaming fashion. This enables proofs for long running executions."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/127268"],"dc:language":["en","eng"],"dc:rights":["Copyright Nishant Rodrigues 2024"],"dc:subject":["Fixpoint","Matching Logic","Logic","Automata"],"dc:title":["Automated reasoning for fixpoints and concrete execution in matching logic"],"dc:type":["text","Thesis"],"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:03Z"}