Verification of a class of loop programs without using loop invariants

zbMATH Open0559.68022MaRDI QIDQ2265799FDOQ2265799

Authors: L. V. Chernobrod 

Publication date: 1984

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

Recommendations

• Elimination of loop invariants in program verification
• Problem-oriented program verification
• Automated generation of loop invariants by recurrence solving in \texttt{Theorema}
• Inadequacy of computable loop invariants
• Problem-oriented approach to verification of file-processing programs

zbMATH Keywords

verificationrecursive functionsloop invariantsHoare's logicstructured loop programs

Mathematics Subject Classification ID

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

Cited In (6)

• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Inferring Loop Invariants Using Postconditions
• A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
• Proving loop termination: Beyond the traditional method
• Verification, Model Checking, and Abstract Interpretation
• Elimination of loop invariants in program verification

This page was built for publication: Verification of a class of loop programs without using loop invariants

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