A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

DOI10.1007/978-3-319-24246-0_9zbMath1471.68119OpenAlexW2295723447MaRDI QIDQ2964458

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (10)

An SMT solver for regular expressions and linear arithmetic over string length ⋮ String theories involving regular membership predicates: from practice to theory and back ⋮ Towards more efficient methods for solving regular-expression heavy string constraints ⋮ Word equations in synergy with regular constraints ⋮ A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings ⋮ An efficient SMT solver for string constraints ⋮ Incremental dead state detection in logarithmic time ⋮ A closer look at the expressive power of logics based on word equations ⋮ Algorithms for checking intersection non-emptiness of regular expressions ⋮ Unification modulo lists with reverse relation with certain word equations

Uses Software

• MONA
• Pex
• Stranger
• HAMPI
• Z3-str
• JST
• S3
• PASS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• From regular expressions to deterministic automata
• Partial derivatives of regular expressions and finite automaton constructions
• A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
• An Evaluation of Automata Algorithms for String Analysis
• Satisfiability of word equations with constants is in PSPACE
• Semi-linear Parikh Images of Regular Expressions via Reduction
• Path Feasibility Analysis for String-Manipulating Programs
• Term Rewriting and All That
• Symbolic Automata Constraint Solving
• Applications of Symbolic Finite Automata
• On Context-Free Languages
• New Computational Paradigms

This page was built for publication: A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings