Automated reasoning for fixpoints and concrete execution in matching logic

Rodrigues, Nishant Joseph

Permalink

https://hdl.handle.net/2142/127268 Copy

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