Elimination of loop invariants in program verification

MaRDI QIDQ1065537zbMATH OpenFDO

Authors V. A. Nepomnyashchij

Publication date 1985

Published in Programming and Computer Software (Search for Journal in Brave)

zbMATH Keywords

eliminating loop invariantsinductive assertionsloop operatorpartial program correctnessverification

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of a class of loop programs without using loop invariants
• Problem-oriented program verification
• On the mechanical derivation of loop invariants
• An iterative method for generating loop invariants
• Mechanical inference of invariants for FOR-loops

Cited in

(17)

• Problem-oriented program verification
• Symbolic verification method for definite iteration over data structures
• On the mechanical derivation of loop invariants
• Effectively eliminating auxiliaries
• A method of proving the invariance of linear inequalities for linear loops
• Verification of a class of loop programs without using loop invariants
• Automatic proving or disproving equality loop invariants based on finite difference techniques
• Loop invariants, exploration of regularities, and mathematical games
• Inferring Loop Invariants Using Postconditions
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• scientific article; zbMATH DE number 3995021 (Why is no real title available?)
• Loop Elimination, a Sound Optimisation Technique for PTTP Related Theorem Proving
• Elimination Techniques for Program Analysis
• Loop invariants: analysis, classification, and examples
• Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs
• Automated Technology for Verification and Analysis
• Reduction and quantifier elimination techniques for program validation

This page was built for publication: Elimination of loop invariants in program verification

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