A note on Presburger arithmetic with array segments, permutation and equality

DOI10.1016/0020-0190(86)90039-6MaRDI QIDQ1073009zbMATH OpenOpenAlexFDO

Authors Louis E. Rosier

Publication date 1986

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(86)90039-6

zbMATH Keywords

satisfiability problemvalidity problemsecond order predicates

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Recommendations

• What's decidable about sequences?
• Verification, Model Checking, and Abstract Interpretation
• What Else Is Decidable about Integer Arrays?
• Decision procedures for extensions of the theory of arrays
• Schemata of formulæ in the theory of arrays

Cites work

• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• A Decision Procedure for the Correctness of a Class of Programs
• Presburger arithmetic with array segments
• Reasoning about arrays
• Verification Decidability of Presburger Array Programs

Cited in

(1)

• Constructing fully symmetric cubature formulae for the sphere

This page was built for publication: A note on Presburger arithmetic with array segments, permutation and equality

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