Verification Decidability of Presburger Array Programs.
Abstract
A program annotated with inductive assertions is said to be verification decidable if all of the verification conditions generated from the program and assertions are formulas in a decidable theory. The Presburger array theory, is defined, containing two logical sorts: integer and array-of-integer. Addition, subtraction, and comparisons are permitted for integers. Array contents and assign functions, and, since the elements of the arrays are integers, array accesses may be nested. The first result is that the validity of unquantified formulas in Presburger array theory is decidable, yet quantified formulas in general are undecidable.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 14, 1977
- Accession Number
- ADA043451
Entities
People
- David Jefferson
- Norihisa Suzuki
Organizations
- Carnegie Mellon University