Symbolic verification method for definite iteration over data structures

DOI10.1016/S0020-0190(99)00009-5MaRDI QIDQ1285767zbMATH OpenFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 1534590
• Symbolic method of verification of definite iterations over altered data structures
• Symbolic verification method for definite iterations over tuples of altered data structures
• scientific article; zbMATH DE number 1822436
• Verification of a finite iteration over data structures

Cites work

• scientific article; zbMATH DE number 3833275 (Why is no real title available?)
• scientific article; zbMATH DE number 3564290 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• A note on the for statement
• An axiomatic basis for computer programming
• Elimination of loop invariants in program verification
• Generalizing specifications for uniformly implemented loops
• Reasoning about arrays
• Some ideas on data types in high-level languages
• Symbolic method of verification of definite iterations over altered data structures

Cited in

(6)

• Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs
• scientific article; zbMATH DE number 1822436 (Why is no real title available?)
• Verification of finite iterations over collections of variable data structures
• Symbolic verification method for definite iterations over tuples of altered data structures
• Symbolic method of verification of definite iterations over altered data structures
• scientific article; zbMATH DE number 1534590 (Why is no real title available?)

Describes a project that uses

Uses Software

• UNITY

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

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