A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
DOI10.1007/978-3-319-24246-0_9zbMATH Open1471.68119OpenAlexW2295723447MaRDI QIDQ2964458FDOQ2964458
Nestan Tsiskaridze, Tianyi Liang, Cesare Tinelli, Clark Barrett, Andrew Reynolds
Publication date: 27 February 2017
Published in: Frontiers of Combining Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-24246-0_9
Formal languages and automata (68Q45) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Partial derivatives of regular expressions and finite automaton constructions
- Satisfiability of word equations with constants is in PSPACE
- On Context-Free Languages
- Term Rewriting and All That
- An Evaluation of Automata Algorithms for String Analysis
- Path Feasibility Analysis for String-Manipulating Programs
- Symbolic Automata Constraint Solving
- From regular expressions to deterministic automata
- A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
- Applications of Symbolic Finite Automata
- New Computational Paradigms
- Semi-linear Parikh Images of Regular Expressions via Reduction
Cited In (12)
- An SMT solver for regular expressions and linear arithmetic over string length
- A decision procedure for string logic with quadratic equations, regular expressions and length constraints
- A closer look at the expressive power of logics based on word equations
- String theories involving regular membership predicates: from practice to theory and back
- Algorithms for checking intersection non-emptiness of regular expressions
- Word equations in synergy with regular constraints
- A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
- Towards more efficient methods for solving regular-expression heavy string constraints
- A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
- Unification modulo lists with reverse relation with certain word equations
- Incremental dead state detection in logarithmic time
- An efficient SMT solver for string constraints
Uses Software
This page was built for publication: A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2964458)
