Further Tackling Post Correspondence Problem and Proof Generation
This program is tentative and subject to change.
Post Correspondence Problem (PCP) is a classic example of an undecidable problem, with various heuristic algorithms proposed to tackle its instances. In this study, we focus on solving a particular subset of instances known as \textit{PCP[3,4]}. We introduce a novel algorithm that leverages regular language and automata theory to identify inductive invariants within the transition systems associated with these instances, enabling us to demonstrate the unsolvability of instances. Additionally, we manually found some inductive invariants using an interactive tool developed specifically for this purpose. As a result, we successfully solved all instances except for three. To ensure the correctness of our results, we generated proofs for each instance that can be verified using Isabelle/HOL.
This program is tentative and subject to change.
Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change
16:00 - 17:30 | |||
16:00 30mTalk | Formalized Burrows-Wheeler Transform CPP Louis Cheung University of Melbourne, Alistair Moffat The University of Melbourne, Christine Rizkallah University of Melbourne | ||
16:30 30mTalk | Verified and Efficient Matching of Regular Expressions with Lookaround CPP Agnishom Chattopadhyay Rice University, Wu Angela Li Rice University, Konstantinos Mamouras Rice University | ||
17:00 30mTalk | Further Tackling Post Correspondence Problem and Proof Generation CPP Akihiro Omori Department of Mathematical and Computing Science, Tokyo Institute of Technology, Yasuhiko Minamide Tokyo Institute of Technology | ||