Decision procedures for sequence theories

DOI10.1007/978-3-031-37703-7_2zbMATH Open1545.68066MaRDI QIDQ6535526FDOQ6535526

Authors: Artur Jeż, Anthony Widjaja Lin, Oliver Markgraf, Philipp Rümmer 

Publication date: 12 January 2024

Recommendations

• What's decidable about sequences?
• A decision procedure for regular membership and length constraints over unbounded strings
• Monadic second-order logic on finite sequences
• An efficient SMT solver for string constraints
• Decision procedures for extensions of the theory of arrays

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Cites Work

• Quicksort
• Title not available (Why is that?)
• Symbolic finite state transducers: algorithms and applications
• Self-stabilizing systems in spite of distributed control
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Verification, Model Checking, and Abstract Interpretation
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• A new solution of Dijkstra's concurrent programming problem
• Software model checking
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Finite-memory automata
• Recompression: a simple and powerful technique for word equations
• Finding all solutions of equations in free groups and monoids with involution
• Variable automata over infinite alphabets
• Makanin's algorithm for word equations-two improvements and a generalization
• Title not available (Why is that?)
• Chain-free string constraints
• Definability in the Existential Theory of Concatenation and Undecidable Extensions of this Theory
• The existential theory of equations with rational constraints in free groups is PSPACE-complete
• The power of symbolic automata and transducers
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• Regular model checking revisited
• A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms
• Symbolic register automata
• On PSPACE generation of a solution set of a word equation and its applications
• What's decidable about sequences?
• Graph logics with rational relations
• On synthesis of specifications with arithmetic
• A solver for arrays with concatenation

This page was built for publication: Decision procedures for sequence theories

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