A Uniform Framework for Handling Position Constraints in String Solving
This program is tentative and subject to change.
We introduce a novel decision procedure for solving the class of position string constraints, which includes string disequalities, $\neg$prefixof, $\neg$suffixof, str.at, and $\neg$str.at. These constraints are generated frequently in almost any application of string constraint solving. Our procedure avoids expensive encoding of the constraints to word equations and, instead, reduces the problem to checking conflicts on positions satisfying an integerconstraint obtained from the Parikh image of a polynomial-sized finite automaton with a special structure. By the reduction to counting, solving position constraints becomes NP-complete and for some cases even falls into PTime. This is much cheaper than the previously used techniques, which either used reductions generating word equations and length constraints (for which modern string solvers use exponential-space
algorithms) or incomplete techniques. Our method is relevant especially for automata-based string solvers, which have recently achieved the best results in terms of practical efficiency, generality, and completeness guarantees. This work allows them to excel also on position constraints, which used to be their weakness. Besides the efficiency gains, we show that our framework may be extended to solve a large fragment of $\neg$contains (in NExpTime), for which decidability has been long open, and gives a hope to solve the general problem. Our implementation of the technique within the Z3-Noodler solver significantly improves its performance on position constraints.
This program is tentative and subject to change.
Thu 19 JunDisplayed time zone: Seoul change
14:00 - 15:00 | |||
14:00 20mTalk | A Uniform Framework for Handling Position Constraints in String Solving PLDI Research Papers Yu-Fang Chen Academia Sinica, Vojtěch Havlena Brno University of Technology, Michal Hečko Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology DOI | ||
14:20 20mTalk | Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus PLDI Research Papers Steven Schaefer University of Michigan, Nathan Varner University of Michigan, Pedro Henrique Azevedo de Amorim University of Oxford, Max S. New University of Michigan DOI Pre-print | ||
14:40 20mTalk | Verifying Solutions to Semantics-Guided Synthesis Problems PLDI Research Papers Charlie Murphy Amazon Web Services, USA, Keith J.C. Johnson University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of California at San Diego DOI |