## Conference paper

Publication language: HABERMEHL Peter, IOSIF Radu and VOJNAR Tomá¹. A Logic of Singly Indexed Arrays. In: Logic for Programming, Artificial Intelligence and Reasoning. Berlin: Springer Verlag, 2008, pp. 558-573. ISBN 978-3-540-89438-4. english A Logic of Singly Indexed Arrays Jednoindexová logika nad poli 558-573 Logic for Programming, Artificial Intelligence and Reasoning 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning -- LPAR'08 LNCS 5330 Berlin, DE 2008 978-3-540-89438-4 Springer Verlag mathematical logic, arrays, decidability, decision procedure, formal verification, automata We present a logic interpreted over integer arrays, which allows difference bound  comparisons between array elements situated within a constant sized window. We show that the satisfiability problem for the logic is undecidable for formulae  with a quantifier prefix \$\{\exists,\forall\}^*\forall^*\exists^*\forall^*\$. For formulae  with quantifier prefixes in the \$\exists^*\forall^*\$ fragment, decidability is established  by an automata-theoretic argument. For each formula in the \$\exists^*\forall^*\$ fragment, we  can build a~flat counter automaton with difference bound transition rules (FCADBM) whose traces correspond to the models of the formula. The construction is modular, following the syntax of  the formula. Decidability of the \$\exists^*\forall^*\$ fragment of the logic is a consequence  of the fact that reachability of a control state is decidable for FCADBM. ```@INPROCEEDINGS{ author = {Peter Habermehl and Radu Iosif and Tom{\'{a}}{\v{s}} Vojnar}, title = {A Logic of Singly Indexed Arrays}, pages = {558--573}, booktitle = {Logic for Programming, Artificial Intelligence and Reasoning}, series = {LNCS 5330}, year = {2008}, location = {Berlin, DE}, publisher = {Springer Verlag}, ISBN = {978-3-540-89438-4}, language = {english}, url = {http://www.fit.vutbr.cz/research/view_pub.php?id=8816} }```