Withdraw
Loading…
Automated reasoning for fixpoints and concrete execution in matching logic
Rodrigues, Nishant Joseph
Loading…
Permalink
https://hdl.handle.net/2142/127268
Description
- Title
- Automated reasoning for fixpoints and concrete execution in matching logic
- Author(s)
- Rodrigues, Nishant Joseph
- Issue Date
- 2024-12-05
- Director of Research (if dissertation) or Advisor (if thesis)
- Rosu, Grigore
- Doctoral Committee Chair(s)
- Rosu, Grigore
- Committee Member(s)
- Meseguer, Jose
- Escobar, Santiago
- Zhang, Lingming
- Department of Study
- Computer Science
- Discipline
- Computer Science
- Degree Granting Institution
- University of Illinois at Urbana-Champaign
- Degree Name
- Ph.D.
- Degree Level
- Dissertation
- Keyword(s)
- fixpoint
- matching logic
- logic
- automata
- Abstract
- 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.
- Graduation Semester
- 2024-12
- Type of Resource
- Thesis
- Handle URL
- https://hdl.handle.net/2142/127268
- Copyright and License Information
- Copyright Nishant Rodrigues 2024
Owning Collections
Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at IllinoisManage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…