TY - JOUR
T1 - Towards a unified proof framework for automated fixpoint reasoning using matching logic
AU - Chen, Xiaohong
AU - Trinh, Minh Thai
AU - Rodrigues, Nishant
AU - Peña, Lucas
AU - Roşu, Grigore
N1 - We warmly thank the anonymous OOPSLA reviewers and our shepherd. Their wit and dedication has helped us improve the presentation. This work was supported in part by NSF CNS 16-19275. This material is based upon work supported by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092. This research is also partly supported by the National Research Foundation, Prime Minister’s Office, Singapore under its Campus for Research Excellence and Technological Enterprise (CREATE) programme.
PY - 2020/11/13
Y1 - 2020/11/13
N2 - 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.
AB - 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.
KW - automated reasoning
KW - fixpoints
KW - induction
KW - matching logic
UR - http://www.scopus.com/inward/record.url?scp=85097582718&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85097582718&partnerID=8YFLogxK
U2 - 10.1145/3428229
DO - 10.1145/3428229
M3 - Article
AN - SCOPUS:85097582718
SN - 2475-1421
VL - 4
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
IS - OOPSLA
M1 - 161
ER -