Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
type: Item
instance of: scholarly article
title: Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
zbMATH Open document ID: 0433.68019
DOI: 10.1016/0304-3975(80)90005-5
author: David Harel
published in: Theoretical Computer Science
publication date: 1980-01-01T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 3675289
zbMATH Keywords: dynamic logic
zbMATH Keywords: invariant assertion method
zbMATH Keywords: termination
zbMATH Keywords: weakest precondition
zbMATH Keywords: intermittent assertion method
zbMATH Keywords: correctness of programs
zbMATH Keywords: deterministic while programs
MaRDI profile type: Publication
full work available at URL: 0304-3975(80)90005-5
OpenAlex ID: W2021907707
cites work: Q4138082
cites work: Lucid—A Formal System for Writing and Proving Programs
cites work: Q3862382
cites work: Q4076735
cites work: On the completeness of the inductive assertion method
cites work: Q4094353
cites work: Q4094352
cites work: Q4130976
cites work: Q4136515
cites work: Q4054648
cites work: Soundness and Completeness of an Axiom System for Program Verification
cites work: Guarded commands, nondeterminacy and formal derivation of programs
cites work: Programming as a Discipline of Mathematical Nature
cites work: Algorithmic properties of structures
cites work: Q5584402
cites work: Proof Theory of Partial Correctness Verification Systems
cites work: First-order dynamic logic
cites work: And/Or Programs: A New Approach to Structured Programming
cites work: On the total correctness of nondeterministic programs
cites work: An axiomatic basis for computer programming
cites work: Some Properties of Predicate Transformers
cites work: Automatic program verification. I: A logical basis and its implementation
cites work: A closer look at termination
cites work: Logical analysis of programs
cites work: Q5585020
cites work: Q4047108
cites work: Q4136521
cites work: Q4151145
cites work: Q4772698
cites work: Q4124327
cites work: Axiomatic approach to total correctness of programs
cites work: Is “sometime” sometimes better than “always”?
cites work: Q5586197
cites work: Q5626601
cites work: Subgoal induction
cites work: Verifying properties of parallel programs
cites work: Q5624635
cites work: Q5596237
cites work: Q4136512
cites work: Axioms for total correctness
cites work: An axiomatic basis for proving total correctness of goto-programs
description: scientific article; zbMATH DE number 3675289