Reasoning about vectors using an SMT theory of sequences

DOI10.1007/978-3-031-10769-6_9OpenAlexW4280549737MaRDI QIDQ2104504

Junkil Park, Cesare Tinelli, Shaz Qadeer, Clark Barrett, Ying Sheng, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Andres Nötzli, Andrew Reynolds

Publication date: 7 December 2022

Full work available at URL: https://arxiv.org/abs/2205.08095

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Reasoning about vectors: satisfiability modulo a theory of sequences

Uses Software

• SMT-LIB
• z3
• CVC4
• Z3str3

Cites Work

• Unnamed Item
• Cardinality constraints for arrays (decidability results and applications)
• Scaling up DPLL(T) string solvers using context-dependent simplification
• Weakly Equivalent Arrays
• Satisfiability Modulo Theories
• Solving SAT and SAT Modulo Theories
• Path Feasibility Analysis for String-Manipulating Programs
• Simplification by Cooperating Decision Procedures
• Polite Theories Revisited
• Splitting on Demand in SAT Modulo Theories
• Frontiers of Combining Systems

This page was built for publication: Reasoning about vectors using an SMT theory of sequences