Automated reasoning for fixpoints and concrete execution in matching logic

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Rodrigues, Nishant Joseph

Contributors dc:contributor

• Rosu, Grigore
• Meseguer, Jose
• Escobar, Santiago
• Zhang, Lingming

• Fixpoint
• Matching Logic
• Logic
• Automata

Statement dc:rights

• Copyright Nishant Rodrigues 2024

Language dc:language

en, eng

Handle dc:identifier

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

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F127268