A decision procedure for string logic with quadratic equations, regular expressions and length constraints

DOI10.1007/978-3-030-02768-1_19zbMATH Open1519.68169OpenAlexW2897835509MaRDI QIDQ6166155FDOQ6166155

Mengda He, Quang Loc Le

Publication date: 2 August 2023

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://research.tees.ac.uk/ws/files/24738048/aplas2018.pdf

Recommendations

• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• A decision procedure for regular membership and length constraints over unbounded strings
• scientific article; zbMATH DE number 1304322
• Chain-free string constraints

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in computer science (03B70) Computational aspects of satisfiability (68R07)

Cited In (8)

• Compositional satisfiability solving in separation logic
• An SMT solver for regular expressions and linear arithmetic over string length
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• A closer look at the expressive power of logics based on word equations
• Word equations in synergy with regular constraints
• Program specialization as a tool for solving word equations
• An efficient cyclic entailment procedure in a fragment of separation logic
• A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

This page was built for publication: A decision procedure for string logic with quadratic equations, regular expressions and length constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166155)