Detail publikace

A Logic of Singly Indexed Arrays

HABERMEHL, P. IOSIF, R. VOJNAR, T.

Originální název

A Logic of Singly Indexed Arrays

Typ

zpráva odborná

Jazyk

angličtina

Originální abstrakt

This report is the full version of an LPAR'08 paper, in which we present a logic interpreted over integer arrays, which allowsdifference bound  comparisons between array elements situated within aconstant sized window. We show that the satisfiability problem for thelogic is undecidable for formulae  with a quantifier prefix$\{\exists,\forall\}^*\forall^*\exists^*\forall^*$. For formulae  withquantifier prefixes in the $\exists^*\forall^*$ fragment, decidabilityis established  by an automata-theoretic argument. For each formula inthe $\exists^*\forall^*$ fragment, we  can build a~flat counterautomaton with difference bound transition rules (FCADBM) whose traces
correspondto the models of the formula. The construction is modular, followingthe syntax of  the formula. Decidability of the $\exists^*\forall^*$fragment of the logic is a consequence  of the fact that reachabilityof a control state is decidable for FCADBM.

Klíčová slova

mathematical logic, arrays, decidability, decision procedure, formal verification, automata

Autoři

HABERMEHL, P.; IOSIF, R.; VOJNAR, T.

Vydáno

3. 12. 2008

Nakladatel

VERIMAG

Místo

TR-2008-9, Grenoble

Strany počet

19

URL

http://www-verimag.imag.fr/TR/TR-2008-9.ps

BibTex

@techreport{BUT63914,
  author="Peter {Habermehl} and Iosif {Radu} and Tomáš {Vojnar}",
  title="A Logic of Singly Indexed Arrays",
  year="2008",
  publisher="VERIMAG",
  address="TR-2008-9, Grenoble",
  pages="19",
  url="http://www-verimag.imag.fr/TR/TR-2008-9.ps"
}