Verification Decidability of Presburger Array Programs

DOI10.1145/322169.322185MaRDI QIDQ3867162zbMATH OpenOpenAlexFDO

Authors Norihisa Suzuki, David Jefferson

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

zbMATH Keywords

data structuresdicision problemsNP-completenessPresburger array theoryprogram verificationtheorem proving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Cited in

(9)

• A note on Presburger arithmetic with array segments, permutation and equality
• Complexity, convexity and combinations of theories
• Presburger arithmetic with array segments
• Array theory of bounded elements and its applications
• Decision procedures for extensions of the theory of arrays
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• The complexity of reversal-bounded model-checking
• Reasoning about reversal-bounded counter machines
• Semantics of algorithmic languages

This page was built for publication: Verification Decidability of Presburger Array Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3867162)