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

verificationinductive assertionseliminating loop invariantsloop operatorpartial program correctness

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

(16)

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

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)