Solving string constraints using SAT

DOI10.1007/978-3-031-37703-7_9zbMATH Open1545.68085MaRDI QIDQ6535533FDOQ6535533

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

Publication date: 12 January 2024

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

Mathematics Subject Classification ID

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

Cites Work

• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• A structure-preserving clause form translation
• Title not available (Why is that?)
• Satisfiability of word equations with constants is in NEXPTIME
• SAT-Based Model Checking without Unrolling
• 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
• Completely non-clausal theorem proving
• Even Faster Conflicts and Lazier Reductions for String Solvers
• 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
• String theories involving regular membership predicates: from practice to theory and back
• Towards more efficient methods for solving regular-expression heavy string constraints
• A survey on operational state complexity
• An SMT solver for regular expressions and linear arithmetic over string length
• On solving word equations using SAT
• Automata-based symbolic string analysis for vulnerability detection
• Relaxations of graph isomorphism
• Solving String Theories Involving Regular Membership Predicates Using SAT
• On strings in software model checking

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)