An efficient SMT solver for string constraints

DOI10.1007/s10703-016-0247-6zbMath1404.68135OpenAlexW2330747214MaRDI QIDQ518402

Cesare Tinelli, Tianyi Liang, Nestan Tsiskaridze, Morgan Deters, Andrew Reynolds, Clark Barrett

Publication date: 28 March 2017

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-016-0247-6

zbMATH Keywords

automated deductionsatisfiability modulo theoriesstring solving

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Active learning of sequential transducers with side information about the domain ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Equational Theorem Proving for Clauses over Strings ⋮ Word equations in synergy with regular constraints ⋮ Unnamed Item ⋮ Completeness of string analysis for dynamic languages

Uses Software

• z3
• Pex
• StarExec
• Stranger
• CVC4
• HAMPI
• Kaluza
• Z3-str
• JST
• S3
• PASS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Hardware and software: verification and testing. 9th international Haifa verification conference, HVC 2013, Haifa, Israel, November 5--7, 2013. Proceedings
• A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
• An Evaluation of Automata Algorithms for String Analysis
• Solving SAT and SAT Modulo Theories
• Satisfiability of word equations with constants is in PSPACE
• Path Feasibility Analysis for String-Manipulating Programs
• Simplification by Cooperating Decision Procedures
• Symbolic Automata Constraint Solving
• Applications of Symbolic Finite Automata
• Splitting on Demand in SAT Modulo Theories