Fifty years of Hoare's logic
From MaRDI portal
Publication:2280214
DOI10.1007/s00165-019-00501-3zbMath1427.68008arXiv1904.03917OpenAlexW2991353706MaRDI QIDQ2280214
Krzysztof R. Apt, Ernst-Ruediger Olderog
Publication date: 18 December 2019
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1904.03917
Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) History of computer science (68-03)
Related Items
Formal semantics of a classical-quantum language, Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs, Logic for reasoning about bugs in loops over data sequences (IFIL), Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs, Extracting total Amb programs from proofs, A predicate transformer for choreographies. Computing preconditions in choreographic programming
Uses Software
Cites Work
- Reduction
- Verifying properties of parallel programs
- Proving the Correctness of Multiprocess Programs
- Generic commands--a tool for partial correctness formalisms
- Parallel programming: An axiomatic approach
- A New Incompleteness Result for Hoare's System
- Soundness and Completeness of an Axiom System for Program Verification
- The Multiple Assignment Statement
- Communicating sequential processes
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Handbook of Model Checking
- Abstraction, Refinement and Proof for Probabilistic Systems
- An Early Program Proof by Alan Turing
- Loop invariants
- Explicit Fair Scheduling for Dynamic Control
- Formal certification of code-based cryptographic proofs
- Formal Methods for Components and Objects
- A contribution to the development of ALGOL
- An axiomatic basis for computer programming
- Proof of a program
- Proof of a recursive program: Quicksort
- Proof of a structured program: 'The sieve of Eratosthenes'
- On Hoare logic and Kleene algebra with tests
- Formal Methods for Open Object-Based Distributed Systems
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Theory and practice of formal methods. Essays dedicated to Frank de Boer on the occasion of his 60th birthday
- Verification of object-oriented programs: a transformational approach
- A Hoare logic for linear systems
- Reasoning about procedures as parameters in the language L4
- Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers
- Toward automatic verification of quantum programs
- Wythoff games, continued fractions, cedar trees and Fibonacci searches
- Fair termination revisited - with delay
- Expressiveness and the completeness of Hoare's logic
- Verification of sequential and concurrent programs
- Formal proof of a program: find
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- Proving total correctness of recursive procedures
- The derivation of systolic computations
- Differential dynamic logic for hybrid systems
- Proof rules and transformations dealing with fairness
- Using branching time temporal logic to synthesize synchronization skeletons
- Ten years of Hoare's logic: A survey. II: Nondeterminism
- A Hoare-like proof system for analysing the computation time of programs
- Two normal form theorems for CSP programs
- Normalform-Transformationen für CSP-Programme. (Normal form transformations for CSP-programs)
- Appraising fairness in languages for distributed programming
- Revised report on the algorithmic language ALGOL 60
- The logic of aliasing
- A calculus of communicating systems
- A proof technique for communicating sequential processes
- Sound and complete Hoare-like calculi based on copy rules
- On termination problems for finitely interpreted ALGOL-like programs
- Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
- A sound and relatively* complete Hoare-logic for a language with higher type procedures
- Pascal. User manual and report. 2nd ed
- An axiomatic proof technique for parallel programs
- Revised report on the algorithmic language ALGOL 68
- Proof rules for the programming language Euclid
- Isabelle/HOL. A proof assistant for higher-order logic
- On the completeness of propositional Hoare logic
- Verified software. Theories, tools, and experiments. 10th international conference, VSTTE 2018, Oxford, UK, July 18--19, 2018. Revised selected papers
- Verifying OpenJDK's sort method for generic collections
- An assertion-based proof system for multithreaded Java
- How the design of JML accommodates both runtime assertion checking and formal verification
- Edinburgh LCF. A mechanized logic of computation
- On the notion of expressiveness and the rule of adaptation
- Rigorous software development. An introduction to program verification.
- Hoare logic and auxiliary variables
- Quicksort revisited. Verifying alternative versions of quicksort
- Hoare logics for time bounds. A study in meta theory
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
- Program proving: KJumps and functions
- An axiomatic definition of the programming language Pascal
- Axiomatic approach to total correctness of programs
- Consistent and complementary formal theories of the semantics of programming languages
- Mathematical Logic for Computer Science
- Probabilistic relational reasoning for differential privacy
- A general framework for sound and complete Floyd-Hoare logics
- VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
- Insight, Inspiration and Collaboration
- Understanding Probabilistic Programs
- Fairness for Infinitary Control
- Simple relational correctness proofs for static analyses and program transformations
- Separation and information hiding
- Counterexample-guided abstraction refinement for symbolic model checking
- Fairness for Dynamic Control
- Modular Verification of Recursive Programs
- Tentative steps toward a development method for interfering programs
- A proof rule for fair termination of guarded commands
- Correctness proofs of distributed termination algorithms
- Effective Axiomatizations of Hoare Logics
- Countable nondeterminism and random assignment
- Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
- Assignment and Procedure Call Proof Rules
- A Proof System for Communicating Sequential Processes
- Ten Years of Hoare's Logic: A Survey—Part I
- Formal Justification of a Proof System for Communicating Sequential Processes
- Guarded commands, nondeterminacy and formal derivation of programs
