Axiomatic approach to total correctness of programs

DOI10.1007/BF00288637zbMath0263.68009WikidataQ56235455 ScholiaQ56235455MaRDI QIDQ2561482

Zohar Manna, Amir Pnueli

Publication date: 1974

Published in: Acta Informatica (Search for Journal in Brave)

Mathematics Subject Classification ID

Formal languages and automata (68Q45) General topics in the theory of software (68N01)

Related Items (11)

On proving the termination of algorithms by machine ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic ⋮ An axiomatic basis for proving total correctness of goto-programs ⋮ Interprocedural shape analysis using separation logic-based transformer summaries ⋮ Fifty years of Hoare's logic ⋮ Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding ⋮ Axiomatic proofs of total correctness of programs ⋮ Current methods for proving program correctness ⋮ Fair termination revisited - with delay ⋮ Constructive design of a hierarchy of semantics of a transition system by abstract interpretation

Uses Software

• Find

Cites Work

• Automatic program verification. I: A logical basis and its implementation
• An axiomatic basis for computer programming
• Proof of a program

This page was built for publication: Axiomatic approach to total correctness of programs