What Else Is Decidable about Integer Arrays?

DOI10.1007/978-3-540-78499-9_33zbMATH Open1139.03007OpenAlexW1859059663MaRDI QIDQ5458380FDOQ5458380

Tomáš Vojnar, Peter Habermehl, Radu Iosif

Publication date: 11 April 2008

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78499-9_33

Recommendations

• A Logic of Singly Indexed Arrays
• Verification, Model Checking, and Abstract Interpretation
• What's decidable about sequences?
• Decision procedures for flat array properties
• Schemata of formulæ in the theory of arrays

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25)

Cited In (14)

• Iterating Octagons
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Algorithmic Analysis of Array-Accessing Programs
• Path Feasibility Analysis for String-Manipulating Programs
• A solver for arrays with concatenation
• Decision procedures for flat array properties
• Verification, Model Checking, and Abstract Interpretation
• When is scalar multiplication decidable?
• Abstraction refinement and antichains for trace inclusion of infinite state systems
• NP satisfiability for arrays as powers
• Relational abstract interpretation of arrays in assembly code
• Inferring complete initialization of arrays
• A note on Presburger arithmetic with array segments, permutation and equality
• A Logic-Based Framework for Reasoning about Composite Data Structures

This page was built for publication: What Else Is Decidable about Integer Arrays?

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