Decision procedures for flat array properties
From MaRDI portal
Recommendations
Cites work
- A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
- A Logic of Singly Indexed Arrays
- An extension of lazy abstraction with interpolation for programs with arrays
- Array Abstractions from Proofs
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Booster: an acceleration-based verification framework for array programs
- Combining nonstably infinite theories
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Computer Aided Verification
- Decision procedures for flat array properties
- Definability of accelerated relations in a theory of arrays and its applications
- Flat Parametric Counter Automata
- Fluid updates: beyond strong vs. weak updates
- scientific article; zbMATH DE number 1954380 (Why is no real title available?)
- scientific article; zbMATH DE number 2090311 (Why is no real title available?)
- scientific article; zbMATH DE number 918133 (Why is no real title available?)
- scientific article; zbMATH DE number 965572 (Why is no real title available?)
- Lazy Abstraction with Interpolants
- Lazy abstraction with interpolants for arrays
- LOGICAL THEORIES OF ONE-PLACE FUNCTIONS ON THE SET OF NATURAL NUMBERS
- Mathematical logic.
- MCMT: a model checker modulo theories
- On Local Reasoning in Verification
- Presburger arithmetic with unary predicates is Π11 complete
- Quantifier instantiation techniques for finite model finding in SMT
- Simplify: a theorem prover for program checking
- The 2013 evaluation of SMT-COMP and SMT-LIB
- Verification, Model Checking, and Abstract Interpretation
- What Else Is Decidable about Integer Arrays?
Cited in
(20)- Cardinality constraints for arrays (decidability results and applications)
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- NP satisfiability for arrays as powers
- Array theory of bounded elements and its applications
- Decision procedures for extensions of the theory of arrays
- Counting constraints in flat array fragments
- Definability of accelerated relations in a theory of arrays and its applications
- Decidability of reachability for polymorphic systems with arrays: a complete classification
- Decision procedures for flat array properties
- Interprocedural reachability for flat integer programs
- Weakly equivalent arrays
- A new acceleration-based combination framework for array properties
- scientific article; zbMATH DE number 6851935 (Why is no real title available?)
- What's decidable about sequences?
- What Else Is Decidable about Integer Arrays?
- A Logic of Singly Indexed Arrays
- Verification, Model Checking, and Abstract Interpretation
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- On algebraic array theories
- An array content static analysis based on non-contiguous partitions
This page was built for publication: Decision procedures for flat array properties
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287272)
