Decision procedures for extensions of the theory of arrays

DOI10.1007/s10472-007-9078-xzbMath1125.68115OpenAlexW2154032363MaRDI QIDQ2457800

Silvio Ghilardi, Daniele Zucchelli, Enrica Nicolini, Silvio Ranise

Publication date: 23 October 2007

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-007-9078-x

zbMATH Keywords

Presburger arithmeticDecision proceduresCombination methodsConstraint satisfiability problemsInstantiation strategiesTheory of arrays with extensionality

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25)

Related Items

NP satisfiability for arrays as powers, Modular instantiation schemes, On algebraic array theories, Interpolation and Symbol Elimination, Theory decision by decomposition, Combination of convex theories: modularity, deduction completeness, and explanation, Array theory of bounded elements and its applications

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-theoretic methods in combined constraint satisfiability
• Presburger arithmetic with array segments
• A rewriting approach to satisfiability procedures.
• Efficient theory combination via Boolean search
• Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
• Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
• Verification Decidability of Presburger Array Programs
• Simplification by Cooperating Decision Procedures
• A Decision Procedure for the Correctness of a Class of Programs
• Assignment Commands with Array References
• Reasoning about arrays
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Computer Science Logic
• Frontiers of Combining Systems
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Logic and structure.