Verification of a class of loop programs without using loop invariants

MaRDI QIDQ2265799zbMATH OpenFDO

Authors L. V. Chernobrod

Publication date 1984

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

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)

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

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)