Solving string constraints using SAT

DOI10.1007/978-3-031-37703-7_9MaRDI QIDQ6535533zbMATHFDO

Authors Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Rupak Majumdar, Dirk Nowotka

Publication date 12 January 2024

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Recommendations

• Solving String Theories Involving Regular Membership Predicates Using SAT
• An efficient SMT solver for string constraints
• High-level abstractions for simplifying extended string constraints in SMT
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Even Faster Conflicts and Lazier Reductions for String Solvers

Cites work

• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A structure-preserving clause form translation
• A survey on operational state complexity
• An SMT solver for regular expressions and linear arithmetic over string length
• Automata-based symbolic string analysis for vulnerability detection
• Completely non-clausal theorem proving
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Even Faster Conflicts and Lazier Reductions for String Solvers
• On solving word equations using SAT
• On strings in software model checking
• Relaxations of graph isomorphism
• SAT-Based Model Checking without Unrolling
• Satisfiability of word equations with constants is in NEXPTIME
• Solving String Theories Involving Regular Membership Predicates Using SAT
• String theories involving regular membership predicates: from practice to theory and back
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Temporal induction by incremental SAT solving
• The expressibility of languages and relations by word equations
• Tools and algorithms for the construction and analysis of systems. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2--7, 2022. Proceedings. Part I
• Towards more efficient methods for solving regular-expression heavy string constraints

Cited in

(1)

• High-level abstractions for simplifying extended string constraints in SMT

This page was built for publication: Solving string constraints using SAT

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