Even Faster Conflicts and Lazier Reductions for String Solvers

DOI10.1007/978-3-031-13188-2_11MaRDI QIDQ6487337zbMATH OpenFDO

Authors Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett, Cesare Tinelli

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-13188-2_11

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• An efficient SMT solver for string constraints
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Scaling up DPLL(T) string solvers using context-dependent simplification
• Towards more efficient methods for solving regular-expression heavy string constraints
• Designing theory solvers with extensions

Cites work

• A mathematical introduction to logic.
• An Evaluation of Automata Algorithms for String Analysis
• Computer Aided Verification
• Fast Decision Procedures Based on Congruence Closure
• High-level abstractions for simplifying extended string constraints in SMT
• Path Feasibility Analysis for String-Manipulating Programs
• Qex: symbolic SQL query explorer
• Satisfiability modulo theories
• Scaling up DPLL(T) string solvers using context-dependent simplification
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Stratified abstraction of access control policies
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• Symbolic automata constraint solving
• 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. Pa

Cited in

(14)

• Designing theory solvers with extensions
• Scaling up DPLL(T) string solvers using context-dependent simplification
• Towards more efficient methods for solving regular-expression heavy string constraints
• scientific article; zbMATH DE number 2043520 (Why is no real title available?)
• An efficient SMT solver for string constraints
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• High-level abstractions for simplifying extended string constraints in SMT
• Word equations in synergy with regular constraints
• Reasoning About Regular Properties: A Comparative Study
• Solving string constraints using SAT
• Incremental algorithms for solving regular expression intersection non-emptiness
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• A faster algorithm for the computation of string convolutions using LZ78 parsing

This page was built for publication: Even Faster Conflicts and Lazier Reductions for String Solvers

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