High-level abstractions for simplifying extended string constraints in SMT

DOI10.1007/978-3-030-25543-5_2MaRDI QIDQ6154871zbMATH OpenOpenAlexFDO

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

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-25543-5_2

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Even Faster Conflicts and Lazier Reductions for String Solvers
• Scaling up DPLL(T) string solvers using context-dependent simplification
• An efficient SMT solver for string constraints
• Solving string constraints using SAT
• Designing theory solvers with extensions

Cited in

(3)

• Flexible proof production in an industrial-strength SMT solver
• Even Faster Conflicts and Lazier Reductions for String Solvers
• Solving string constraints using SAT

This page was built for publication: High-level abstractions for simplifying extended string constraints in SMT

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