Decision procedures for sequence theories

DOI10.1007/978-3-031-37703-7_2MaRDI QIDQ6535526zbMATH OpenFDO

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

Publication date 12 January 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37703-7_2

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(2)

• Complementable normal form of parametrized automata
• Reasoning over n-indexed sequences in SMT

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)