Reasoning about procedures as parameters in the language L4

DOI10.1016/0890-5401(89)90040-0zbMath0692.68011OpenAlexW1990487099MaRDI QIDQ583874

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

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)90040-0

zbMATH Keywords

completenessaxiom systemexpressivenessreasoning about programsAlgol-like languagelanguage L4partial correctness assertionsprocedures passed as parameters

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items

Complexity of proving program correctness, Horn Clause Solvers for Program Verification, Semantics and reasoning with free procedures, Fifty years of Hoare's logic

Cites Work

• Correctness of programs with Pascal-like procedures without global variables
• On termination problems for finitely interpreted ALGOL-like programs
• A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programs
• On relative completeness of Hoare logics
• The characterization problem for Hoare logics
• Effective Axiomatizations of Hoare Logics
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item