On algebraic array theories

DOI10.1016/J.JLAMP.2023.100906MaRDI QIDQ6192058zbMATH OpenOpenAlexFDO

Authors R. Raja, Viktor Kuncak

Publication date 12 February 2024

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

arrayscomposition theoremsdecision proceduresFeferman-Vaughtsatisfiability modulo theories

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• Algorithmic uses of the Feferman-Vaught theorem
• Array Folds Logic
• Automata, Languages and Programming
• Booster: an acceleration-based verification framework for array programs
• Carathéodory bounds for integer cones
• Cardinality constraints for arrays (decidability results and applications)
• Combining theories with shared set operations
• Computational Complexity
• Cosmological lower bound on the circuit complexity of a small problem in logic
• Dafny: an automatic program verifier for functional correctness
• Deciding Boolean algebra with Presburger arithmetic
• Decision procedures for extensions of the theory of arrays
• Decision procedures for flat array properties
• Decision procedures. An algorithmic point of view
• From regular expressions to DFA's using compressed NFA's
• scientific article; zbMATH DE number 53151 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• On direct products of theories
• Ordered sets in the calculus of data structures
• Refinement types for Haskell
• The computational complexity of logical theories
• The first order properties of products of algebraic systems
• The monadic second order theory of all countable ordinals
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• Verification, Model Checking, and Abstract Interpretation
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(2)

• Succinct ordering and aggregation constraints in algebraic array theories
• Modular derivation of decision procedures for extensions of the algebraic theory of arrays

This page was built for publication: On algebraic array theories

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