Succinct ordering and aggregation constraints in algebraic array theories
From MaRDI portal
Publication:6561348
DOI10.1016/J.JLAMP.2024.100978MaRDI QIDQ6561348FDOQ6561348
Authors: R. Raja, Viktor Kuncak 
Publication date: 25 June 2024
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Cites Work
- Dafny: an automatic program verifier for functional correctness
- Refinement types for Haskell
- Title not available (Why is that?)
- Computational Complexity
- Title not available (Why is that?)
- Carathéodory bounds for integer cones
- Simplification by Cooperating Decision Procedures
- Title not available (Why is that?)
- Sets with cardinality constraints in satisfiability modulo theories
- An application of games to the completeness problem for formalized theories
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Weak Second‐Order Arithmetic and Finite Automata
- On the complexity of integer programming
- Cosmological lower bound on the circuit complexity of a small problem in logic
- Automated Deduction – CADE-20
- Tree acceptors and some of their applications
- The first order properties of products of algebraic systems
- Forward and backward application of symbolic tree transducers
- Tree Automata over Infinite Alphabets
- The monadic second order theory of all countable ordinals
- The computational complexity of logical theories
- Combining theories with shared set operations
- Symbolic automata constraint solving
- Automata, Languages and Programming
- Symbolic tree automata
- Decision procedures. An algorithmic point of view
- On direct products of theories
- Deciding Boolean algebra with Presburger arithmetic
- Efficient automated reasoning about sets and multisets with cardinality constraints
- Solving \(\mathrm{LIA}^\star\) using approximations
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Linear Arithmetic with Stars
- Logics with aggregate operators
- Minimization of Symbolic Tree Automata
- Ordered sets in the calculus of data structures
- Cardinality constraints for arrays (decidability results and applications)
- NP satisfiability for arrays as powers
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Array Folds Logic
- Decision Procedures for Automating Termination Proofs
- Variants and satisfiability in the infinitary unification wonderland
- On algebraic array theories
This page was built for publication: Succinct ordering and aggregation constraints in algebraic array theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6561348)
