Reasoning about vectors using an SMT theory of sequences

DOI10.1007/978-3-031-10769-6_9MaRDI QIDQ2104504zbMATH OpenOpenAlexFDO

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

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

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)

Cites work

• A mathematical introduction to logic.
• Cardinality constraints for arrays (decidability results and applications)
• Frontiers of Combining Systems
• Path Feasibility Analysis for String-Manipulating Programs
• Polite theories revisited
• Satisfiability modulo theories
• Scaling up DPLL(T) string solvers using context-dependent simplification
• Simplification by Cooperating Decision Procedures
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Splitting on Demand in SAT Modulo Theories
• Weakly equivalent arrays

Cited in

(5)

• Verifying SQL queries using theories of tables and relations
• Reasoning about vectors: satisfiability modulo a theory of sequences
• Polite combination in parametric array theories
• A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
• Rely-guarantee reasoning for causally consistent shared memory

Describes a project that uses

Uses Software

• Z3str3
• CVC4
• z3
• SMT-LIB

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

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