Ten Years of Hoare's Logic: A Survey—Part I

No abstract is available for this paper.

• Publication year

  1981

• Venue

  ACM Transactions on Programming Languages and Systems

• Publication date

  1981-10-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/357146.357150
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Expressiveness and the Completeness of Hoare's Logic

  1982cited by this paper
• Some Natural Structures which Fail to Possess a Sound and Decidable Hoare-Like Logic for their While-Programs

  1982cited by this paper
• Ten years of Hoare''s logic: A survey

  1981cited by this paper
• Mathematical theory of program correctness

  1980influential reference
• Definability in Dynamic Logic

  1980cited by this paper
• Present-Day Hoare-Like Systems for Programming Languages with Procedures: Power, Limits and most Likely Expressions

  1980cited by this paper
• Assignment and Procedure Call Proof Rules

  1980cited by this paper
• Proving the Correctness of Regular Deterministic Programs: A Unifying Survey Using Dynamic Logic

  1980cited by this paper
• First-Order Dynamic Logic

  1979cited by this paper
• Recursive Assertions are not enough - or are they?

  1979cited by this paper
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems

  1979influential reference
• A New Incompleteness Result for Hoare's System

  1978cited by this paper
• The Multiple Assignment Statement

  1978cited by this paper
• Soundness and Completeness of an Axiom System for Program Verification

  1978influential reference
• Unrestricted procedure calls in Hoare's logic

  1978cited by this paper
• Proving the correctness of coroutines without history variables

  1978cited by this paper
• On a theory of decision problems in programming languages

  1978influential reference
• Program invariants as fixed points

  1977cited by this paper
• Semantics and Proof Theory of Pascal Procedures

  1977influential reference
• Total Correctness for Procedures

  1977cited by this paper
• On the proper treatment of referencing, dereferencing and assignment : (preprint)

  1977cited by this paper
• A necessary and sufficient condition for the existence of hoare logics

  1977cited by this paper
• Exercises in Denotational Semantics

  1976cited by this paper
• Completeness and Incompleteness Theorems for Hoare-like Axiom Systems

  1976cited by this paper
• A Discipline of Programming

  1976influential reference
• SEMANTICAL CONSIDERATIONS ON FLOYD-HOARE LOGIC

  1976cited by this paper
• Proving assertions about programs that manipulate data structures

  1975cited by this paper
• On the Most Recent Property of Algol-Like Programs

  1974cited by this paper
• The “most recent” error: Its causes and correction

  1972cited by this paper
• Consistent formal theories of the semantics of programming languages

  1971cited by this paper
• Procedures and parameters: An axiomatic approach

  1971influential reference
• An axiomatic basis for computer programming

  1969influential reference
• Mathematical logic

  1967cited by this paper
• A contribution to the development of ALGOL

  1966cited by this paper

• History-Based Reasoning about Behavioral Subtyping (extended paper)

  2026cites this paper
• Verifying Almost-Sure Termination for Randomized Distributed Algorithms

  2026cites this paper
• Cyclic Proofs in Hoare Logic and its Reverse

  2025cites this paper
• Access Hoare Logic

  2025cites this paper
• Unified Analysis Techniques for Programs with Outcomes

  2024cites this paper
• Automated Software Verification of Hyperliveness

  2024cites this paper
• Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects

  2024influential citation
• Sound and Complete Proof Rules for Probabilistic Termination

  2024cites this paper
• (AUTOMATED) LISTENING IS MORE MEANINGFUL WITH THE SOURCE CODE

  2023cites this paper
• Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning

  2023cites this paper
• A Generalized Hybrid Hoare Logic

  2023cites this paper
• ON THE SEMANTICS OF DIGITAL AUDIO WORKSTATIONS AS PROGRAM INTERPRETERS

  2023cites this paper
• Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation

  2023cites this paper
• Revealing Sources of (Memory) Errors via Backward Analysis

  2023influential citation
• Toward Tool-Independent Summaries for Symbolic Execution

  2023cites this paper
• An Analysis of How Many Undiscovered Vulnerabilities Remain in Information Systems

  2023cites this paper
• Monoidal Hoare Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning

  2022cites this paper
• Unrealizability Logic

  2022influential citation
• Dijkstra’s Legacy on Program Verification

  2022cites this paper
• Composition-Nominative Methods and Models in Program Development

  2022cites this paper
• Reasoning about Recursive Quantum Programs

  2021cites this paper
• Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic

  2021cites this paper
• Reasoning about Recursive antum Programs

  2021cites this paper
• A Small-Step Operational Semantics for GP 2

  2021cites this paper
• On Algebra of Program Correctness and Incorrectness

  2021cites this paper
• R-Calculi for Modal Logic

  2021cites this paper
• Sequent Calculi of First-order Logics of Partial Predicates with Extended Renominations and Composition of Predicate Complement

  2020cites this paper
• Information and Communication Technologies in Education, Research, and Industrial Applications: 15th International Conference, ICTERI 2019, Kherson, Ukraine, June 12–15, 2019, Revised Selected Papers

  2020cites this paper
• Automated reasoning and randomization in separation logic

  2020influential citation
• Understanding Programming Languages

  2020cites this paper
• Language evolution and healthiness for critical cyber‐physical systems

  2020cites this paper
• Thirty-seven years of relational Hoare logic: remarks on its principles and history

  2020cites this paper
• Programming Languages and Systems: 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 – December 2, 2020, Proceedings

  2020cites this paper
• Formal Verification of Atomicity Requirements for Smart Contracts

  2020cites this paper
• Automated urban train control with hybrid Event-B: 'Tackling' the rugby club problem

  2020cites this paper
• Relations of Logical Consequence in Program-oriented Logics of Quasiary Predicates

  2020cites this paper
• Probabilistic Couplings from Program Logics

  2020cites this paper
• First-order composition-nominative logics with predicates of weak equality and of strong equality

  2019cites this paper
• Fifty years of Hoare’s logic

  2019influential citation
• Formal specification and verification

  2019cites this paper
• Comparative Analysis of Approaches to Static Verification of Dynamic Memory

  2019influential citation
• Program-Oriented Logics of Renominative Level with Extended Renomination and Equality

  2019cites this paper
• Review of Recent Techniques on Heap Specification and Verification

  2019cites this paper
• A Denotational Engineering of Programming Languages

  2019cites this paper
• A First-Order Logic with Frames

  2019cites this paper
• Timed Automata for Security of Real-Time Systems

  2019cites this paper
• Bunched logics: a uniform approach

  2019cites this paper
• Renominative logics with extended renomination, equality and predicate complement

  2019cites this paper
• Program Logics of Renominative Level with the Composition of Predicate Complement

  2019cites this paper
• Relational and algebraic methods in computer science

  2019cites this paper
• Program Logics Based on Algebras with the Composition of Predicate Complement

  2019cites this paper
• Resource semantics: logic as a modelling technology

  2019cites this paper
• Incorrectness logic

  2019cites this paper
• The power of modal separation logics

  2019cites this paper
• Reasoning About Shared-Variable Concurrency: Interactions Between Research Threads

  2019cites this paper
• Towards Verifying Ethereum Smart Contracts at Intermediate Language Level

  2019cites this paper
• Reasoning about call-by-value: a missing result in the history of Hoare's logic

  2019cites this paper
• Completeness and expressiveness of pointer program verification by separation logic

  2019cites this paper
• A Hoare Logic Contract Theory: An Exercise in Denotational Semantics

  2018cites this paper
• Beyond Structured Programming

  2018cites this paper
• We Need a Testability Transformation Semantics

  2018cites this paper
• Induction-based Verification of Synchronous and Hybrid Programs

  2018cites this paper
• Why Separation Logic Works

  2018cites this paper
• On the Sequence Rule for the Floyd-Hoare Logic with Partial Pre- and Post-Conditions

  2018cites this paper
• Inference Rules for the Partial Floyd-Hoare Logic Based on Composition of Predicate Complement

  2018cites this paper
• Combining Model Checking and Deduction

  2018cites this paper
• Verification of Program Parallelization

  2018cites this paper
• Principled Software Development

  2018influential citation
• Techniques for the verification of dynamically typed programs

  2017cites this paper
• Information Flow for Timed Automata

  2017cites this paper
• Engineering Trustworthy Software Systems

  2017cites this paper
• On Completeness Results of Hoare Logic Relative to the Standard Model

  2017cites this paper
• Hoare-Style Reasoning from Multiple Contracts

  2017influential citation
• Inferring Formal Properties of Production Key-Value Stores

  2017cites this paper
• An Approach To Formalization of an Extension of Floyd-Hoare Logic

  2017cites this paper
• Formalizing Hoare Logic in PVS

  2017cites this paper
• Extended Floyd-Hoare Logic over Relational Nominative Data

  2017cites this paper
• Completeness of Hoare Logic Relative to the Standard Model

  2017cites this paper
• Atomistic Galois insertions for flow sensitive integrity

  2017cites this paper
• Probabilistic Couplings for Probabilistic Reasoning

  2017influential citation
• SCHOOL OF COMPUTING Title : Challenges for semantic description : Comparing responses from the main approaches Names :

  2017cites this paper
• BCS Formal Aspects of Computing Command Algebras , Recursion and Program Transformation

  2017cites this paper
• Content dependent information flow control

  2017cites this paper
• Challenges for Formal Semantic Description: Responses from the Main Approaches

  2017cites this paper
• Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism

  2016cites this paper
• Reasoning about actions with loops via Hoare logic

  2016cites this paper
• The M-computations induced by accessibility relations in nonstandard models M of Hoare logic

  2016cites this paper
• A Single-Assignment Translation for Annotated Programs

  2016cites this paper
• Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

  2016cites this paper
• Program Verification: To Err is Human

  2016cites this paper
• The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes

  2016influential citation
• Fine-grained Information Flow for Concurrent Computation

  2016cites this paper
• A unified framework for metering cloud environments

  2016cites this paper
• Completeness of Hoare logic with inputs over the standard model

  2016cites this paper
• Effectively Eliminating Auxiliaries

  2016cites this paper
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach

  2016cites this paper
• Semantics, Logic, and Verification of "Exact Real Computation"

  2016cites this paper
• Feferman-Landin Logic

  2016cites this paper
• Computabilidad, complejidad computacional y verificación de programas

  2016cites this paper
• Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction

  2016influential citation