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

DOI10.1016/0020-0190(86)90039-6zbMATH Open0588.03007OpenAlexW2059490901MaRDI QIDQ1073009FDOQ1073009

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Presburger arithmetic with array segments
• Verification Decidability of Presburger Array Programs
• Reasoning about arrays
• A Decision Procedure for the Correctness of a Class of 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)