The unwind property for programs with bounded memory

DOI10.1016/0020-0190(85)90090-0MaRDI QIDQ1067771zbMATH OpenOpenAlexFDO

Authors Assaf Kfoury

Publication date 1985

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

Full work available at URL https://doi.org/10.1016/0020-0190(85)90090-0

zbMATH Keywords

definability by programsflowchart programslogics of programsprogram schemesrecursiontruth-table propertyunbounded memoryunwind property

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

For programs that can access unbounded memory (e.g., flowchart programs with recursion on simple variable parameters), the 'unwind property' is equivalent to the 'truth-table property'. For programs restricted to bounded memory (e.g., flowchart programs with parameters recursion), the two properties are not equivalent in general. We recapitulate all known results, give new results, and establish conditions under which the two properties are equivalent for program with bounded memory.

Recommendations

• Unbounded program memory adds to the expressive power of first-order programming logic
• scientific article; zbMATH DE number 3845026
• scientific article; zbMATH DE number 16457
• Undecidable boundedness problems for datalog programs
• Unwinding Conditions for Security in Imperative Languages

Cites work

• Definability by deterministic and non-deterministic programs (with applications to first-order dynamic logic)
• Definability by programs in first-order structures
• Deterministic dynamic logic is strictly weaker than dynamic logic
• scientific article; zbMATH DE number 3858392 (Why is no real title available?)
• scientific article; zbMATH DE number 3890697 (Why is no real title available?)
• scientific article; zbMATH DE number 3778723 (Why is no real title available?)
• scientific article; zbMATH DE number 3788603 (Why is no real title available?)
• scientific article; zbMATH DE number 3789816 (Why is no real title available?)
• scientific article; zbMATH DE number 3492141 (Why is no real title available?)
• scientific article; zbMATH DE number 3892551 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• Nontrivial definability by flow-chart programs
• Theory of program structures: Schemes, semantics, verification

This page was built for publication: The unwind property for programs with bounded memory

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