Ten Years of Hoare's Logic: A Survey—Part I
From MaRDI portal
Publication:3925144
DOI10.1145/357146.357150zbMath0471.68006OpenAlexW2111619838MaRDI QIDQ3925144
Publication date: 1981
Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/357146.357150
parameterscompletenessexpressivenesssoundnesspartial correctnessrecursive procedurescall-by-valuetotal correctnessprocedurescall-by-namearithmetical interpretationwhile programssubscripted variablesvariable declarationscall-by-variabledynamic scopestatic scope
Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)
Related Items
Non-standard algorithmic and dynamic logic, Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction, The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes, Process algebra with guards: Combining hoare logic with process algebra, A model and temporal proof system for networks of processes, Partial correctness of exits from concurrent structures, Stratified least fixpoint logic, Completeness for recursive procedures in separation logic, Reasoning about dynamically evolving process structures, Kleene's three-valued logic and process algebra, Weakest preconditions for pure Prolog programs, Combining Model Checking and Deduction, Hoare Logic for Disjunctive Information Flow, Verification conditions are code, Specification and verification challenges for sequential object-oriented programs, On simulation, subtyping and substitutability in sequential object systems, Some general incompleteness results for partial correctness logics, Semantics and verification of monitors and systems of monitors and processes, Arithmetical completeness versus relative completeness, A methodology for designing proof rules for fair parallel programs, Partial hyperdoctrines: categorical models for partial function logic and Hoare logic, A language independent proof of the soundness and completeness of generalized Hoare logic, Weak second order characterizations of various program verification systems, Program composition via unification, A theory of implementation and refinement in timed Petri nets, An observationally complete program logic for imperative higher-order functions, A first order logic of effects, Completeness and expressiveness of pointer program verification by separation logic, Completeness of Hoare logic with inputs over the standard model, Liminf progress measures, Hoare logic for Java in Isabelle/HOL, On algebra of program correctness and incorrectness, Issues in the design of a parallel object-oriented language, Completeness of Hoare Logic Relative to the Standard Model, Command algebras, recursion and program transformation, Proving total correctness of recursive procedures, A transformational characterization of if-then-else, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, Observable behavior of distributed systems: component reasoning for concurrent objects, Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism, On termination problems for finitely interpreted ALGOL-like programs, The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic, Reasoning about actions with loops via Hoare logic, On the completeness of modular proof systems, Proof obligations for blocks and procedures, Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language, A sound and complete reasoning system for asynchronous communication with shared futures, Verification conditions for source-level imperative programs, Hoare's logic and Peano's arithmetic, A mechanical analysis of program verification strategies, Completing the temporal picture, Decidability of a partial order based temporal logic, A proof system for adaptable class hierarchies, Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule, Term rewriting and Hoare logic -- Coded rewriting, On the logic of UNITY, Content dependent information flow control, A natural deduction approach to dynamic logic, On the status of proving program properties in effective interpretations, Verification of Concurrent Systems with VerCors, Bochvar-McCarthy logic and process algebra, Existential Fixed-Point Logic, Universal Quantifiers, and Topoi, Incremental reasoning with lazy behavioral subtyping for multiple inheritance, A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs, Lazy behavioral subtyping, Reasoning about Recursive Processes in Shared-Variable Concurrency, Verification of concurrent programs: The automata-theoretic framework, Reasoning about procedures as parameters in the language L4, Incremental Reasoning for Multiple Inheritance, Fifty years of Hoare's logic, A Hoare logic for dynamic networks of asynchronously communicating deterministic processes, Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach, A shared-variable concurrency analysis of multi-threaded object-oriented programs, Verifying traits: an incremental proof system for fine-grained reuse, Process algebra with four-valued logic, Hoare's logic and VDM, Reverse Hoare Logic, Proving possibility properties, Wythoff games, continued fractions, cedar trees and Fibonacci searches, Generating algebraic laws from imperative programs, A logical analysis of aliasing in imperative higher-order functions, Completeness of Hoare-calculi revisited, On the notion of expressiveness and the rule of adaptation, A proof outline logic for object-oriented programming, Correctness of programs with Pascal-like procedures without global variables, Two theorems about the completeness of Hoare's logic, Hoare's logic for programming languages with two data types, Ten years of Hoare's logic: A survey. II: Nondeterminism, Expressiveness and the completeness of Hoare's logic, The axiomatic semantics of programs based on Hoare's logic, Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects, Some questions about expressiveness and relative completeness in Hoare's logic, On the completeness of propositional Hoare logic, A complete axiomatic semantics of spawning, The completeness of functional logic, Calculating sharp adaptation rules.
