On algebraic array theories

DOI10.1016/j.jlamp.2023.100906OpenAlexW4386365754MaRDI QIDQ6192058

Rodrigo Raya, Viktor Kuncak

Publication date: 12 February 2024

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2023.100906

zbMATH Keywords

arrayssatisfiability modulo theoriesdecision procedurescomposition theoremsFeferman-Vaught

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decision procedures for flat array properties
• Decision procedures. An algorithmic point of view
• Algorithmic uses of the Feferman-Vaught theorem
• Deciding Boolean algebra with Presburger arithmetic
• The monadic second order theory of all countable ordinals
• The computational complexity of logical theories
• From regular expressions to DFA's using compressed NFA's
• Cardinality constraints for arrays (decidability results and applications)
• Decision procedures for extensions of the theory of arrays
• Carathéodory bounds for integer cones
• Refinement types for Haskell
• Dafny: An Automatic Program Verifier for Functional Correctness
• The first order properties of products of algebraic systems
• Weak Second‐Order Arithmetic and Finite Automata
• Cosmological lower bound on the circuit complexity of a small problem in logic
• Booster: An Acceleration-Based Verification Framework for Array Programs
• Ordered Sets in the Calculus of Data Structures
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• Combining Theories with Shared Set Operations
• Array Folds Logic
• Computational Complexity
• Automata, Languages and Programming
• On direct products of theories
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: On algebraic array theories