The Power of Regular Constraint Propagation
This program is tentative and subject to change.
The past decade has witnessed substantial developments in string solving. Motivated by the complexity of string solving strategies adopted in existing string solvers, we investigate a simple and generic method for solving string constraints: regular constraint propagation. The method repeatedly computes pre- or post-images of regular languages under the string functions present in a string formula, inferring more and more knowledge about the possible values of string variables, until either a conflict is found or satisfiability of the string formula can be concluded. Such a propagation strategy is applicable to string constraints with multiple operations like concatenation, replace, and almost all flavors of string transductions. We demonstrate the generality and effectiveness of this method theoretically and experimentally. On the theoretical side, we show that RCP is sound and complete for a large fragment of string constraints, subsuming both straight-line and chain-free constraints, which are the hitherto largest decidable fragments of string constraints supported by string solvers. On the practical side, we implement regular constraint propagation within the open-source string solver OSTRICH. Our experimental evaluation shows that this addition significantly improves OSTRICH’s performance and makes it competitive with existing solvers. In fact, it substantially outperforms other solvers on random PCP and bioinformatics benchmarks. The results also suggest that incorporating regular constraint propagation alongside other techniques could lead to substantial performance gains for existing solvers.
This program is tentative and subject to change.
Thu 16 OctDisplayed time zone: Perth change
13:45 - 15:30 | |||
13:45 15mTalk | A Unifying Approach to Product Constructions for Quantitative Temporal Inference OOPSLA Kazuki Watanabe National Institute of Informatics; SOKENDAI, Sebastian Junges Radboud University, Jurriaan Rot Radboud University Nijmegen, Ichiro Hasuo National Institute of Informatics, Japan | ||
14:00 15mTalk | Contract System Metatheories à la Carte: A Transition-System View of Contracts OOPSLA Shu-Hung You Northwestern University, USA, Christos Dimoulas Northwestern University, Robert Bruce Findler Northwestern University | ||
14:15 15mTalk | Incremental Bidirectional Typing via Order Maintenance OOPSLA Thomas J. Porter University of Michigan, Marisa Kirisame University of Utah, Ivan Wei University of Michigan, Pavel Panchekha University of Utah, Cyrus Omar University of Michigan | ||
14:30 15mTalk | The Power of Regular Constraint Propagation OOPSLA Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin RPTU Kaiserslautern-Landau and Max-Planck Institute for Software Systems, Oliver Markgraf RPTU Kaiserslautern-Landau, Philipp Ruemmer University of Regensburg and Uppsala University | ||
14:45 15mTalk | Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles OOPSLA Zhineng Zhong Key Laboratory of High-Confidence Software Technologies (MOE), School of Computer Science, Peking University, Ziqi Zhang University of Illinois Urbana-Champaign, Hanqin Guan Peking University, Ding Li Peking University | ||
15:00 15mTalk | Software Model Checking via Summary-Guided Search OOPSLA Ruijie Fang University of Texas at Austin, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI Pre-print |