SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Thu 16 Oct 2025 14:30 - 14:45 at Orchid Plenary Ballroom - Systems

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 Oct

Displayed time zone: Perth change

13:45 - 15:30
13:45
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
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