Technická zpráva

HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008.
Jazyk publikace:angličtina
Název publikace:What else is decidable about integer arrays?
Název (cs):Co dále je rozhodnutelné o polích?
Strany:36
Místo vydání:TR-2007-8, Grenoble, FR
Rok:2008
Vydavatel:VERIMAG
URL:http://www.fit.vutbr.cz/~vojnar/Publications/hiv-arrays-tr-07.pdf [PDF]
Klíčová slova
mathematical logic, arrays, decidability, decision procedure, formal verification, automata
Anotace
Tato zpráva je úplnou verzí článku publikovaného na FOSSACS'08, zahrnující mj. důkazy. Tento článek zavádí novou logiku nad předem neomezenými poli neomezených celočíselných údajů a ukazuje, že splnitelnost formulí této logiky je rozhodnutelná. Tato logika je $\exists^* \forall^*$ fragmentem predikátové logiky prvního řádu a umožňuje (1) presburgerovské omezení nad existenčně kvantifikovanými indexy, (2) diferenční omezení i omezení periodicity nad univerzálně kvantifikovanými indexy a (3) diferenční omezení nad hodnotami uloženými v polích. Zavedená rozhodovací procedura, založená na využití teorie automatů, může být uplatněna v rámci nástrojů pro automatickou formální verifikaci programů.
BibTeX:
@TECHREPORT{
   author = {Peter Habermehl and Radu Iosif and Tomáš Vojnar},
   title = {What else is decidable about integer arrays?},
   pages = {36},
   year = {2008},
   location = {TR-2007-8, Grenoble, FR},
   publisher = {VERIMAG},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=8819}
}

Vaše IPv4 adresa: 54.163.70.249
Přepnout na IPv6 spojení

DNSSEC [dnssec]