A language independent proof of the soundness and completeness of generalized Hoare logic

DOI10.1016/0890-5401(89)90018-7zbMath0676.68004OpenAlexW2014375692MaRDI QIDQ1122978

Patrick Cousot, Radhia Cousot

Publication date: 1989

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(89)90018-7

zbMATH Keywords

Hoare logicreasoning about programsprogram verificiation

Mathematics Subject Classification ID

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

Related Items

S-semantics for logic programming: a retrospective look

Cites Work

• Unnamed Item
• The Hoare logic of concurrent programs
• Ten years of Hoare's logic: A survey. II: Nondeterminism
• Proving assertions about parallel programs
• The ``Hoare Logic of CSP, and All That
• Ten Years of Hoare's Logic: A Survey—Part I
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• An axiomatic basis for computer programming