Symbolic verification method for definite iteration over data structures

DOI10.1016/S0020-0190(99)00009-5zbMath0917.68020MaRDI QIDQ1285767

V. A. Nepomniaschy

Publication date: 28 April 1999

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

zbMATH Keywords

Program correctnessDefinite iterationProof ruleVerification method

Mathematics Subject Classification ID

Data structures (68P05) General topics in the theory of software (68N01)

Related Items (2)

Verification of finite iterations over collections of variable data structures ⋮ Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Elimination of loop invariants in program verification
• Symbolic method of verification of definite iterations over altered data structures
• Some ideas on data types in high-level languages
• Reasoning about arrays
• Generalizing specifications for uniformly implemented loops
• An axiomatic basis for computer programming
• A note on the for statement

This page was built for publication: Symbolic verification method for definite iteration over data structures