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