What Else Is Decidable about Integer Arrays?

DOI10.1007/978-3-540-78499-9_33MaRDI QIDQ5458380zbMATH OpenOpenAlexFDO

Authors Peter Habermehl, Radu Iosif, Tomáš Vojnar

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

Mathematics Subject Classification ID

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

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

Cited in

(18)

• Iterating Octagons
• What's decidable about sequences?
• 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
• Decision procedures for flat array properties
• A solver for arrays with concatenation
• Array theory of bounded elements and its applications
• A Logic of Singly Indexed Arrays
• 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
• Counting constraints in flat array fragments
• 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)