Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
DOI10.1145/322108.322121zbMATH Open0388.68008OpenAlexW2140295918WikidataQ114614039 ScholiaQ114614039MaRDI QIDQ4170195FDOQ4170195
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
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)
- Complexity of proving program correctness
- The Birth of Model Checking
- Ernst-Rüdiger Olderog: A Life for Meaning
- Program invariants as fixedpoints
- Specifications in an arbitrary institution
- Arithmetical completeness versus relative completeness
- Verification conditions are code
- Fifty years of Hoare's logic
- Horn clause solvers for program verification
- 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
- Reasoning about procedures as parameters in the language L4
- Verification of object-oriented programs: a transformational approach
- Correctness of programs with Pascal-like procedures without global variables
- On the Completeness of Dynamic Logic
- On termination problems for finitely interpreted ALGOL-like programs
- Hierarchical development of programming languages
- Completeness of algorithmic logic
- Average case optimality for linear problems
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
- Semantics of algorithmic languages
- A Hoare-like verification system for a language with an exception handling mechanism
- Stratified least fixpoint logic
- Semantics and reasoning with free procedures
- Proving program inclusion using Hoare's logic
- 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
- Completeness of Hoare-calculi revisited
- On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
- SMT-based model checking for recursive programs
- Wythoff games, continued fractions, cedar trees and Fibonacci searches
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)
