Co dále je rozhodnutelné o polích?

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F08%3APU78080" target="_blank" >RIV/00216305:26230/08:PU78080 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

What else is decidable about integer arrays?

Popis výsledku v původním jazyce

This report is the full version of the corresponding FOSSCAS'08 paper, including full proofs of the achived results. In the work, we introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the $exists^* forall^*$ first-order fragment and allows (1) Presburger constraints on existentially quantified variables, (2) difference constraints as well as periodicity constraints on universally quantified indices, and (3) difference constraints on values. In particular,using our logic, one can express constraints on consecutive elements of arrays (e.g., $forall i ~.~ 0 leq i &lt; n rightarrow a[i+1]=a[i]-1$) as well as periodic facts (e.g., $forall i ~.~ i equiv_2 0 rightarrow a[i] = 0$). The decision procedure follows the automata-theoretic approach: we translate formulae into a special class of B&quot;uchi counter automata such that any model of a formula corresponds to an accepting run of an automaton, and vice versa. The emptiness problem fo

Název v anglickém jazyce

What else is decidable about integer arrays?

Popis výsledku anglicky

This report is the full version of the corresponding FOSSCAS'08 paper, including full proofs of the achived results. In the work, we introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the $exists^* forall^*$ first-order fragment and allows (1) Presburger constraints on existentially quantified variables, (2) difference constraints as well as periodicity constraints on universally quantified indices, and (3) difference constraints on values. In particular,using our logic, one can express constraints on consecutive elements of arrays (e.g., $forall i ~.~ 0 leq i &lt; n rightarrow a[i+1]=a[i]-1$) as well as periodic facts (e.g., $forall i ~.~ i equiv_2 0 rightarrow a[i] = 0$). The decision procedure follows the automata-theoretic approach: we translate formulae into a special class of B&quot;uchi counter automata such that any model of a formula corresponds to an accepting run of an automaton, and vice versa. The emptiness problem fo

Druh

A - Audiovizuální tvorba

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GA102%2F07%2F0322" target="_blank" >GA102/07/0322: Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2008

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

—

Místo vydání

—

Název nakladatele resp. objednatele

—

Verze

—

Identifikační číslo nosiče

—