Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems

DOI10.1145/322108.322121MaRDI QIDQ4170195zbMATH OpenOpenAlexWikidataFDO

Authors Edmund Clarke

Publication date 1979

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

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computability and recursion theory on ordinals, admissible sets, etc. (03D60) Algorithms in computer science (68W99)

Cited in

(32)

• Proving program inclusion using Hoare's logic
• The Birth of Model Checking
• Semantics and reasoning with free procedures
• On termination problems for finitely interpreted ALGOL-like programs
• Verification of object-oriented programs: a transformational approach
• Reasoning about procedures as parameters in the language L4
• Stratified least fixpoint logic
• Semantics of algorithmic languages
• Wythoff games, continued fractions, cedar trees and Fibonacci searches
• On the notion of expressiveness and the rule of adaptation
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• Average case optimality for linear problems
• Fifty years of Hoare's logic
• On the Completeness of Dynamic Logic
• Completeness of Hoare-calculi revisited
• Verification conditions are code
• Specifications in an arbitrary institution
• Correctness of programs with Pascal-like procedures without global variables
• On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
• Ernst-Rüdiger Olderog: A Life for Meaning
• A Hoare-like verification system for a language with an exception handling mechanism
• Hierarchical development of programming languages
• Program invariants as fixedpoints
• Arithmetical completeness versus relative completeness
• Completeness of algorithmic logic
• Horn clause solvers for program verification
• SMT-based model checking for recursive programs
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Completeness of Hoare logic relative to the standard model
• An observationally complete program logic for imperative higher-order functions
• Expressiveness and the completeness of Hoare's logic
• Complexity of proving program correctness

This page was built for publication: Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4170195)