Fifty years of Hoare's logic (Q2280214): Difference between revisions

@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CESAR
@@ Property / describes a project that uses: CESAR / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+KIV
@@ Property / describes a project that uses: KIV / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Quicksort
@@ Property / describes a project that uses: Quicksort / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Eiffel
@@ Property / describes a project that uses: Eiffel / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ALGOL 60
@@ Property / describes a project that uses: ALGOL 60 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Z
@@ Property / describes a project that uses: Z / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Find
@@ Property / describes a project that uses: Find / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2991353706
@@ Property / OpenAlex ID: W2991353706 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.03917
@@ Property / arXiv ID: 1904.03917 / rank @@
+Normal rank
@@ Property / cites work @@
+Two normal form theorems for CSP programs
@@ Property / cites work: Two normal form theorems for CSP programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4124296
@@ Property / cites work: Q4124296 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving total correctness of recursive procedures
@@ Property / cites work: Proving total correctness of recursive procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Q3997397
@@ Property / cites work: Q3997397 / rank @@
+Normal rank
@@ Property / cites work @@
+An assertion-based proof system for multithreaded Java
+Normal rank
@@ Property / cites work @@
+Modular Verification of Recursive Programs
@@ Property / cites work: Modular Verification of Recursive Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Verification of sequential and concurrent programs
+Normal rank
@@ Property / cites work @@
+Verification of object-oriented programs: a transformational approach
+Normal rank
@@ Property / cites work @@
+A Proof System for Communicating Sequential Processes
+Normal rank
@@ Property / cites work @@
+Appraising fairness in languages for distributed programming
+Normal rank
@@ Property / cites work @@
+Rigorous software development. An introduction to program verification.
+Normal rank
@@ Property / cites work @@
+A general framework for sound and complete Floyd-Hoare logics
+Normal rank
@@ Property / cites work @@
+A Hoare logic for linear systems
@@ Property / cites work: A Hoare logic for linear systems / rank @@
+Normal rank
@@ Property / cites work @@
+Proof rules and transformations dealing with fairness
+Normal rank
@@ Property / cites work @@
+Q3999717
@@ Property / cites work: Q3999717 / rank @@
+Normal rank
@@ Property / cites work @@
+Countable nondeterminism and random assignment
@@ Property / cites work: Countable nondeterminism and random assignment / rank @@
+Normal rank
@@ Property / cites work @@
+Fair termination revisited - with delay
@@ Property / cites work: Fair termination revisited - with delay / rank @@
+Normal rank
@@ Property / cites work @@
+Ten Years of Hoare's Logic: A Survey—Part I
@@ Property / cites work: Ten Years of Hoare's Logic: A Survey—Part I / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Justification of a Proof System for Communicating Sequential Processes
+Normal rank
@@ Property / cites work @@
+Ten years of Hoare's logic: A survey. II: Nondeterminism
+Normal rank
@@ Property / cites work @@
+Correctness proofs of distributed termination algorithms
+Normal rank
@@ Property / cites work @@
+Q3898009
@@ Property / cites work: Q3898009 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5291078
@@ Property / cites work: Q5291078 / rank @@
+Normal rank
@@ Property / cites work @@
+Simple relational correctness proofs for static analyses and program transformations
+Normal rank
@@ Property / cites work @@
+Mathematical Logic for Computer Science
@@ Property / cites work: Mathematical Logic for Computer Science / rank @@
+Normal rank
@@ Property / cites work @@
+Q3791123
@@ Property / cites work: Q3791123 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal certification of code-based cryptographic proofs
+Normal rank
@@ Property / cites work @@
+Probabilistic relational reasoning for differential privacy
+Normal rank
@@ Property / cites work @@
+Q2746874
@@ Property / cites work: Q2746874 / rank @@
+Normal rank
@@ Property / cites work @@
+A semantics for concurrent separation logic
@@ Property / cites work: A semantics for concurrent separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
+Normal rank
@@ Property / cites work @@
+Expressiveness and the completeness of Hoare's logic
+Normal rank
@@ Property / cites work @@
+Quicksort revisited. Verifying alternative versions of quicksort
+Normal rank
@@ Property / cites work @@
+Effective Axiomatizations of Hoare Logics
@@ Property / cites work: Effective Axiomatizations of Hoare Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Counterexample-guided abstraction refinement for symbolic model checking
+Normal rank
@@ Property / cites work @@
+Program proving: KJumps and functions
@@ Property / cites work: Program proving: KJumps and functions / rank @@
+Normal rank
@@ Property / cites work @@
+Q5417200
@@ Property / cites work: Q5417200 / rank @@
+Normal rank
@@ Property / cites work @@
+Handbook of Model Checking
@@ Property / cites work: Handbook of Model Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
+Normal rank
@@ Property / cites work @@
+The logic of aliasing
@@ Property / cites work: The logic of aliasing / rank @@
+Normal rank
@@ Property / cites work @@
+Soundness and Completeness of an Axiom System for Program Verification
+Normal rank
@@ Property / cites work @@
+Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
+Normal rank
@@ Property / cites work @@
+Q3999156
@@ Property / cites work: Q3999156 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3899466
@@ Property / cites work: Q3899466 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods for Components and Objects
@@ Property / cites work: Formal Methods for Components and Objects / rank @@
+Normal rank
@@ Property / cites work @@
+Q5684216
@@ Property / cites work: Q5684216 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994464
@@ Property / cites work: Q3994464 / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying OpenJDK's sort method for generic collections
+Normal rank
@@ Property / cites work @@
+Theory and practice of formal methods. Essays dedicated to Frank de Boer on the occasion of his 60th birthday
+Normal rank
@@ Property / cites work @@
+VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
+Normal rank
@@ Property / cites work @@
+Guarded commands, nondeterminacy and formal derivation of programs
+Normal rank
@@ Property / cites work @@
+Q4144755
@@ Property / cites work: Q4144755 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3962450
@@ Property / cites work: Q3962450 / rank @@
+Normal rank
@@ Property / cites work @@
+A sound and relatively* complete Hoare-logic for a language with higher type procedures
+Normal rank
@@ Property / cites work @@
+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
+Normal rank
@@ Property / cites work @@
+Q2768503
@@ Property / cites work: Q2768503 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692630
@@ Property / cites work: Q4692630 / rank @@
+Normal rank
@@ Property / cites work @@
+Using branching time temporal logic to synthesize synchronization skeletons
+Normal rank
@@ Property / cites work @@
+Proof of a recursive program: Quicksort
@@ Property / cites work: Proof of a recursive program: Quicksort / rank @@
+Normal rank
@@ Property / cites work @@
+Formal proof of a program: find
@@ Property / cites work: Formal proof of a program: find / rank @@
+Normal rank
@@ Property / cites work @@
+Q5584402
@@ Property / cites work: Q5584402 / rank @@
+Normal rank
@@ Property / cites work @@
+Loop invariants
@@ Property / cites work: Loop invariants / rank @@
+Normal rank
@@ Property / cites work @@
+Q3738540
@@ Property / cites work: Q3738540 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4003356
@@ Property / cites work: Q4003356 / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning about procedures as parameters in the language L4
+Normal rank
@@ Property / cites work @@
+A proof rule for fair termination of guarded commands
+Normal rank
@@ Property / cites work @@
+Assignment and Procedure Call Proof Rules
@@ Property / cites work: Assignment and Procedure Call Proof Rules / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+The Multiple Assignment Statement
@@ Property / cites work: The Multiple Assignment Statement / rank @@
+Normal rank
@@ Property / cites work @@
+Q3925859
@@ Property / cites work: Q3925859 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3731019
@@ Property / cites work: Q3731019 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4525781
@@ Property / cites work: Q4525781 / rank @@
+Normal rank
@@ Property / cites work @@
+Consistent and complementary formal theories of the semantics of programming languages
+Normal rank
@@ Property / cites work @@
+Hoare logics for time bounds. A study in meta theory
+Normal rank
@@ Property / cites work @@
+An axiomatic basis for computer programming
@@ Property / cites work: An axiomatic basis for computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q5626277
@@ Property / cites work: Q5626277 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof of a program
@@ Property / cites work: Proof of a program / rank @@
+Normal rank
@@ Property / cites work @@
+Q4772697
@@ Property / cites work: Q4772697 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof of a structured program: 'The sieve of Eratosthenes'
+Normal rank
@@ Property / cites work @@
+Parallel programming: An axiomatic approach
@@ Property / cites work: Parallel programming: An axiomatic approach / rank @@
+Normal rank
@@ Property / cites work @@
+Communicating sequential processes
@@ Property / cites work: Communicating sequential processes / rank @@
+Normal rank
@@ Property / cites work @@
+Fairness for Dynamic Control
@@ Property / cites work: Fairness for Dynamic Control / rank @@
+Normal rank
@@ Property / cites work @@
+Fairness for Infinitary Control
@@ Property / cites work: Fairness for Infinitary Control / rank @@
+Normal rank
@@ Property / cites work @@
+An axiomatic definition of the programming language Pascal
+Normal rank
@@ Property / cites work @@
+Tentative steps toward a development method for interfering programs
+Normal rank
@@ Property / cites work @@
+Insight, Inspiration and Collaboration
@@ Property / cites work: Insight, Inspiration and Collaboration / rank @@
+Normal rank
@@ Property / cites work @@
+Pascal. User manual and report. 2nd ed
@@ Property / cites work: Pascal. User manual and report. 2nd ed / rank @@
+Normal rank
@@ Property / cites work @@
+The derivation of systolic computations
@@ Property / cites work: The derivation of systolic computations / rank @@
+Normal rank
@@ Property / cites work @@
+Understanding Probabilistic Programs
@@ Property / cites work: Understanding Probabilistic Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Hoare logic and auxiliary variables
@@ Property / cites work: Hoare logic and auxiliary variables / rank @@
+Normal rank
@@ Property / cites work @@
+On Hoare logic and Kleene algebra with tests
@@ Property / cites work: On Hoare logic and Kleene algebra with tests / rank @@
+Normal rank
@@ Property / cites work @@
+On the completeness of propositional Hoare logic
@@ Property / cites work: On the completeness of propositional Hoare logic / rank @@
+Normal rank
@@ Property / cites work @@
+Proving the Correctness of Multiprocess Programs
@@ Property / cites work: Proving the Correctness of Multiprocess Programs / rank @@
+Normal rank
@@ Property / cites work @@
+On termination problems for finitely interpreted ALGOL-like programs
+Normal rank
@@ Property / cites work @@
+How the design of JML accommodates both runtime assertion checking and formal verification
+Normal rank
@@ Property / cites work @@
+Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers
+Normal rank
@@ Property / cites work @@
+A proof technique for communicating sequential processes
+Normal rank
@@ Property / cites work @@
+Proof rules for the programming language Euclid
@@ Property / cites work: Proof rules for the programming language Euclid / rank @@
+Normal rank
@@ Property / cites work @@
+Reduction
@@ Property / cites work: Reduction / rank @@
+Normal rank
@@ Property / cites work @@
+Q3851570
@@ Property / cites work: Q3851570 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3883459
@@ Property / cites work: Q3883459 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3922147
@@ Property / cites work: Q3922147 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3995530
@@ Property / cites work: Q3995530 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4124327
@@ Property / cites work: Q4124327 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4371400
@@ Property / cites work: Q4371400 / rank @@
+Normal rank
@@ Property / cites work @@
+A calculus of communicating systems
@@ Property / cites work: A calculus of communicating systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q3992568
@@ Property / cites work: Q3992568 / rank @@
+Normal rank
@@ Property / cites work @@
+An Early Program Proof by Alan Turing
@@ Property / cites work: An Early Program Proof by Alan Turing / rank @@
+Normal rank
@@ Property / cites work @@
+Abstraction, Refinement and Proof for Probabilistic Systems
+Normal rank
@@ Property / cites work @@
+Q4301161
@@ Property / cites work: Q4301161 / rank @@
+Normal rank
@@ Property / cites work @@
+Axiomatic approach to total correctness of programs
+Normal rank
@@ Property / cites work @@
+Q4002642
@@ Property / cites work: Q4002642 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3792662
@@ Property / cites work: Q3792662 / rank @@
+Normal rank
@@ Property / cites work @@
+Revised report on the algorithmic language ALGOL 60
+Normal rank
@@ Property / cites work @@
+A Hoare-like proof system for analysing the computation time of programs
+Normal rank
@@ Property / cites work @@
+Q4823141
@@ Property / cites work: Q4823141 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4411818
@@ Property / cites work: Q4411818 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+An axiomatic proof technique for parallel programs
+Normal rank
@@ Property / cites work @@
+Verifying properties of parallel programs
@@ Property / cites work: Verifying properties of parallel programs / rank @@
+Normal rank
@@ Property / cites work @@
+Resources, concurrency, and local reasoning
@@ Property / cites work: Resources, concurrency, and local reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Sound and complete Hoare-like calculi based on copy rules
+Normal rank
@@ Property / cites work @@
+On the notion of expressiveness and the rule of adaptation
+Normal rank
@@ Property / cites work @@
+Wythoff games, continued fractions, cedar trees and Fibonacci searches
+Normal rank
@@ Property / cites work @@
+Explicit Fair Scheduling for Dynamic Control
@@ Property / cites work: Explicit Fair Scheduling for Dynamic Control / rank @@
+Normal rank
@@ Property / cites work @@
+Q4783297
@@ Property / cites work: Q4783297 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4140351
@@ Property / cites work: Q4140351 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4151147
@@ Property / cites work: Q4151147 / rank @@
+Normal rank
@@ Property / cites work @@
+Separation and information hiding
@@ Property / cites work: Separation and information hiding / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods for Open Object-Based Distributed Systems
+Normal rank
@@ Property / cites work @@
+Differential dynamic logic for hybrid systems
@@ Property / cites work: Differential dynamic logic for hybrid systems / rank @@
+Normal rank
@@ Property / cites work @@
+Verified software. Theories, tools, and experiments. 10th international conference, VSTTE 2018, Oxford, UK, July 18--19, 2018. Revised selected papers
+Normal rank
@@ Property / cites work @@
+Q3940830
@@ Property / cites work: Q3940830 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5596237
@@ Property / cites work: Q5596237 / rank @@
+Normal rank
@@ Property / cites work @@
+Generic commands--a tool for partial correctness formalisms
+Normal rank
@@ Property / cites work @@
+Q4134897
@@ Property / cites work: Q4134897 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3995087
@@ Property / cites work: Q3995087 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4039815
@@ Property / cites work: Q4039815 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4501670
@@ Property / cites work: Q4501670 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4808824
@@ Property / cites work: Q4808824 / rank @@
+Normal rank
@@ Property / cites work @@
+Revised report on the algorithmic language ALGOL 68
+Normal rank
@@ Property / cites work @@
+A New Incompleteness Result for Hoare's System
@@ Property / cites work: A New Incompleteness Result for Hoare's System / rank @@
+Normal rank
@@ Property / cites work @@
+A contribution to the development of ALGOL
@@ Property / cites work: A contribution to the development of ALGOL / rank @@
+Normal rank
@@ Property / cites work @@
+Q3141916
@@ Property / cites work: Q3141916 / rank @@
+Normal rank
@@ Property / cites work @@
+Toward automatic verification of quantum programs
@@ Property / cites work: Toward automatic verification of quantum programs / rank @@
+Normal rank
@@ Property / cites work @@
+Normalform-Transformationen für CSP-Programme. (Normal form transformations for CSP-programs)
+Normal rank
@@ Property / Wikidata QID @@
+Q130841271
@@ Property / Wikidata QID: Q130841271 / rank @@
+Normal rank