Problem-oriented program verification

MaRDI QIDQ1082069zbMATH OpenFDO

Authors V. A. Nepomnyashchij

Publication date 1986

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

zbMATH Keywords

correctnessgoto statementloopsequential and parallel replacement in arraystransformation

Mathematics Subject Classification ID

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

Review text

We describe a methodology of problem-oriented program verification which includes a special invariant-free derivation rule for a loop writing into a file, an identity condition for sequential and parallel replacement in arrays, which simplifies the proof of correctness conditions, and also a transformation to remove the goto statement from the body of a loop.

Recommendations

• Problem-oriented approach to verification of file-processing programs
• Problem-oriented program verification system ?SPEKTR?
• Elimination of loop invariants in program verification
• Verification of procedural programs
• Program verification: state of the art, problems, and results. I

Cited in

(14)

• Elimination of loop invariants in program verification
• Problem-oriented approach to verification of file-processing programs
• Problem-oriented verification system and its application to linear algebra programs
• A unified approach of program verification
• Verification of a class of loop programs without using loop invariants
• A new approach to program verification
• Programmed strategies for program verification
• A vindication of program verification
• scientific article; zbMATH DE number 3881857 (Why is no real title available?)
• Problem-oriented program verification system ?SPEKTR?
• scientific article; zbMATH DE number 53100 (Why is no real title available?)
• A compositional proof system for distributed programs
• Program verification through characteristic formulae
• Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs

This page was built for publication: Problem-oriented program verification

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