A decision procedure for regular membership and length constraints over unbounded strings

DOI10.1007/978-3-319-24246-0_9MaRDI QIDQ2964458zbMATH OpenOpenAlexFDO

Authors Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark Barrett

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) 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)

Recommendations

• An efficient SMT solver for string constraints
• A decision procedure for string logic with quadratic equations, regular expressions and length constraints
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Solving String Theories Involving Regular Membership Predicates Using SAT
• Chain-free string constraints

Cites work

• scientific article; zbMATH DE number 3577484 (Why is no real title available?)
• scientific article; zbMATH DE number 2043550 (Why is no real title available?)
• scientific article; zbMATH DE number 1773084 (Why is no real title available?)
• scientific article; zbMATH DE number 2090837 (Why is no real title available?)
• A decision procedure for regular membership and length constraints over unbounded strings
• An Evaluation of Automata Algorithms for String Analysis
• Applications of symbolic finite automata
• From regular expressions to deterministic automata
• New Computational Paradigms
• On Context-Free Languages
• Partial derivatives of regular expressions and finite automaton constructions
• Path Feasibility Analysis for String-Manipulating Programs
• Satisfiability of word equations with constants is in PSPACE
• Semi-linear Parikh Images of Regular Expressions via Reduction
• Symbolic automata constraint solving
• Term Rewriting and All That

Cited in

(17)

• 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
• Incremental algorithms for solving regular expression intersection non-emptiness
• A decision procedure for regular membership and length constraints over unbounded strings
• 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
• Unbounded model-checking with interpolation for regular language constraints
• Word equations in synergy with regular constraints
• A symbolic algorithm for the case-split rule in string constraint solving
• 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
• Chain-free string constraints
• Decision procedures for sequence theories
• Incremental dead state detection in logarithmic time
• An efficient SMT solver for string constraints

Describes a project that uses

Uses Software

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

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)