Detail publikace
A Logic of Singly Indexed Arrays
Jedná se úplnou verzi článku publikovaného na LPAR'08. Článek zavádí specializovanou logiku pro specifikaci vlastností programů pracujících s poli neomezené velikosti obsahující celočíselné údaje o rovněž neomezené velikosti. Tato logika se vyznačuje tím, že umožňuje v jedné, univerzálně kvantifikované formuli porovnávat obsah různých buněk polí pouze s využitím jediného sdíleného indexu. Pro tuto logiku je v článku ukázána obecná nerozhodnutelnost splnitelnosti formulí. Na druhou stranu pro $\exists^*\forall^*$ fragment této logiky je navržena rozhodovací procedura založená na určitém speciálním typu automatů s čítači. Oproti dřívějším výsledkům v této oblasti je navržená rozhodovací procedura výrazně jednodušší.
@TECHREPORT{FITPUB8817, author = "Peter Habermehl and Radu Iosif and Tom\'{a}\v{s} Vojnar", title = "A Logic of Singly Indexed Arrays", pages = 19, year = 2008, location = "TR-2008-9, Grenoble, FR", publisher = "VERIMAG", language = "english", url = "https://www.fit.vut.cz/research/publication/8817" }