Verification Decidability of Presburger Array Programs
From MaRDI portal
Publication:3867162
DOI10.1145/322169.322185zbMath0429.68025OpenAlexW2092518806MaRDI QIDQ3867162
David Jefferson, Norihisa Suzuki
Publication date: 1980
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://figshare.com/articles/journal_contribution/Verification_decidability_of_Presburger_array_programs/6612710
theorem provingNP-completenessdata structuresprogram verificationdicision problemsPresburger array theory
Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)
Related Items (8)
The Complexity of Reversal-Bounded Model-Checking ⋮ Equivalence between model-checking flat counter systems and Presburger arithmetic ⋮ Complexity, convexity and combinations of theories ⋮ Presburger arithmetic with array segments ⋮ Decision procedures for extensions of the theory of arrays ⋮ Semantics of algorithmic languages ⋮ Array theory of bounded elements and its applications ⋮ A note on Presburger arithmetic with array segments, permutation and equality
This page was built for publication: Verification Decidability of Presburger Array Programs
