Reasoning about vectors: satisfiability modulo a theory of sequences

DOI10.1007/s10817-023-09682-2OpenAlexW4386776668MaRDI QIDQ6053845

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

Publication date: 24 October 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-023-09682-2

zbMATH Keywords

sequencessatisfiability modulo theoriesdecision proceduresvectors

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Cardinality constraints for arrays (decidability results and applications)
• Reasoning about vectors using an SMT theory of sequences
• Scaling up DPLL(T) string solvers using context-dependent simplification
• Interpolation and amalgamation for arrays with MaxDiff
• Weakly Equivalent Arrays
• Satisfiability Modulo Theories
• Solving SAT and SAT Modulo Theories
• Path Feasibility Analysis for String-Manipulating Programs
• Proving termination with multiset orderings
• 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: satisfiability modulo a theory of sequences