Current methods for proving program correctness

DOI10.1007/BF01069058zbMath0461.68020MaRDI QIDQ3911363

I. V. Kasatkina, E. L. Yushchenko

Publication date: 1980

Published in: Cybernetics (Search for Journal in Brave)

zbMATH Keywords

program correctness

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

Uses Software

• COBOL
• Find

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about programs
• Proving assertions about parallel programs
• Automatic program verification. I: A logical basis and its implementation
• Mathematical theory of partial correctness
• Program proving: KJumps and functions
• Axiomatic approach to total correctness of programs
• Consistent and complementary formal theories of the semantics of programming languages
• An axiomatic basis for proving total correctness of goto-programs
• Verifying properties of parallel programs
• Formal verification of parallel programs
• Proving Theorems about LISP Functions
• Logical analysis of programs
• Parallel programming: An axiomatic approach
• A New Incompleteness Result for Hoare's System
• Prospects and Limitations of Automatic Assertion Generation for Loop Programs
• Soundness and Completeness of an Axiom System for Program Verification
• Inductive methods for proving properties of programs
• Proving Properties of Programs by Structural Induction
• An axiomatic basis for computer programming
• Formalization of Properties of Functional Programs
• Proof of a program
• Another recursion induction principle