Difference between revisions of "Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic"

From FSL
Jump to: navigation, search
 
Line 1: Line 1:
 +
== OOPSLA 2020 ==
 +
<pubbib id='chen-pena-rodrigues-rosu-trinh-2020-oopsla' template='PubDefaultWithAbstractAndTitle'/>
 
== Technical Report ==
 
== Technical Report ==
 
<pubbib id='chen-pena-rodrigues-rosu-trinh-2020-tr' template='PubDefaultWithAbstractAndTitle'/>
 
<pubbib id='chen-pena-rodrigues-rosu-trinh-2020-tr' template='PubDefaultWithAbstractAndTitle'/>
<private>
 
== OOPSLA 2020 Submission ==
 
<pubbib id='chen-pena-rodrigues-rosu-trinh-2020-oopsla-submission' template='PubDefaultWithAbstractAndTitle'/>
 
</private>
 
 
<private>
 
<private>
 
== PLDI 2020 Submission ==
 
== PLDI 2020 Submission ==

Latest revision as of 03:44, 15 October 2020

[edit] OOPSLA 2020

Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic
Xiaohong Chen and Minh-Thai Trinh and Nishant Rodrigues and Lucas Pena and Grigore Rosu
OOPSLA'20, ACM/IEEE, pp 1-29. 2020
Abstract. Automation of fixpoint reasoning has been extensively studied for various mathematical structures, logical formalisms, and computational domains, resulting in specialized fixpoint provers for heaps, for streams, for term algebras, for temporal properties, for program correctness, and for many other formal systems and inductive and coinductive properties. However, in spite of great theoretical and practical interest, there is no unified framework for automated fixpoint reasoning. Although several attempts have been made, there is no evidence that such a unified framework is possible, or practical. In this paper, we propose a candidate based on matching logic, a formalism recently shown to theoretically unify the above mentioned formal systems. Unfortunately, the (Knaster-Tarski) proof rule of matching logic, which enables inductive reasoning, is not syntax-driven. Worse, it can be applied at any step during a proof, making automation seem hopeless. Inspired by recent advances in automation of inductive proofs in separation logic, we propose an alternative proof system for matching logic, which is amenable for automation. We then discuss our implementation of it, which although not superior to specialized state-of-the-art automated provers for specific domains, we believe brings some evidence and hope that a unified framework for automated reasoning is not out of reach.
PDF, Matching Logic, OOPSLA'20, BIB

[edit] Technical Report

Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic
Xiaohong Chen and Minh-Thai Trinh and Nishant Rodrigues and Lucas Pena and Grigore Rosu
Technical Report http://hdl.handle.net/2142/108369, September 2020
Abstract. Automation of fixpoint reasoning has been extensively studied for various mathematical structures, logical formalisms, and computational domains, resulting in specialized fixpoint provers for heaps, for streams, for term algebras, for temporal properties, for program correctness, and for many other formal systems and inductive and coinductive properties. However, in spite of great theoretical and practical interest, there is no unified framework for automated fixpoint reasoning. Although several attempts have been made, there is no evidence that such a unified framework is possible, or practical. In this paper, we propose a candidate based on matching logic, a formalism recently shown to theoretically unify the above mentioned formal systems. Unfortunately, the (Knaster-Tarski) proof rule of matching logic, which enables inductive reasoning, is not syntax-driven. Worse, it can be applied at any step during a proof, making automation seem hopeless. Inspired by recent advances in automation of inductive proofs in separation logic, we propose an alternative proof system for matching logic, which is amenable for automation. We then discuss our implementation of it, which although not superior to specialized state-of-the-art automated provers for specific domains, we believe brings some evidence and hope that a unified framework for automated reasoning is not out of reach.
PDF, Matching Logic, DOI, BIB


Personal tools
Namespaces

Variants
Actions
Navigation