A Constraint Solving Approach to Parikh Images of Regular Languages
A common problem in string constraint solvers is computing the Parikh image, a linear arithmetic formula that describes all possible combinations of character counts in strings of a given language. Automata-based string solvers frequently need to compute the Parikh image of large products (intersections) of nondeterministic automata, which in many operations is both prohibitively slow and memory-intensive. We contribute a novel understanding of how Parikh maps can be tackled as a constraint solving problem to solve real-world constraints stemming from functions on regular languages, including length and indexing constraints. Furthermore, we show how this formulation can be efficiently implemented as a calculus, PC*, in an automated theorem prover supporting Presburger logic. We implement PC* in a tool called Catra, and evaluate it on constraints produced by the Ostrich+ string constraint solver when solving Parikh automata intersection problems produced when solving standard string constraint benchmarks involving cardinality constraints on strings. We show that our solution strictly outperforms the standard approach described in Verma et al. as well as the over-approximating method recently described by Janků and Turoňová by a wide margin, and for realistic timeouts for constraint solving also the nuXmv model checker.
Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:40 | Formal Methods 2OOPSLA 2024 at San Gabriel Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
16:00 20mTalk | A Constraint Solving Approach to Parikh Images of Regular Languages OOPSLA 2024 DOI | ||
16:20 20mTalk | Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing OOPSLA 2024 Wenjia Ye National University of Singapore, Yaozhu Sun University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
16:40 20mTalk | Inductive diagrams for causal reasoning OOPSLA 2024 Jonathan Castello University of California, Santa Cruz, Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California, Santa Cruz DOI Pre-print | ||
17:00 20mTalk | Message-Observing Sessions OOPSLA 2024 DOI | ||
17:20 20mTalk | Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels OOPSLA 2024 Si Liu ETH Zurich, Long Gu State Key Laboratory for Novel Software Technology, Nanjing University, Hengfeng Wei State Key Laboratory for Novel Software Technology, Nanjing University, David Basin ETH Zurich DOI |