Effective Axiomatizations of Hoare Logics

DOI10.1145/2402.322394zbMath0627.68010OpenAlexW2063113502MaRDI QIDQ3763566

Steven M. German, Joseph Y. Halpern, Edmund M. Clarke

Publication date: 1983

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2402.322394

zbMATH Keywords

programming languageshalting problemfinite interpretationsexpressive interpretationsLipton's theorempartial- correctnesssound and relatively complete axiomatization expressivenesstermination assertionstotal-correctness assertions

Mathematics Subject Classification ID

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

Related Items (11)

Arithmetical completeness versus relative completeness ⋮ The Birth of Model Checking ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ On termination problems for finitely interpreted ALGOL-like programs ⋮ Semantics and reasoning with free procedures ⋮ On the status of proving program properties in effective interpretations ⋮ Reasoning about procedures as parameters in the language L4 ⋮ Fifty years of Hoare's logic ⋮ Wythoff games, continued fractions, cedar trees and Fibonacci searches ⋮ Correctness of programs with Pascal-like procedures without global variables ⋮ Weakly expressive models for Hoare logic

This page was built for publication: Effective Axiomatizations of Hoare Logics