This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Relatively complete, and no better
A subject the papers are about. The loosest grouping, and the one to reach for last.
What a program logic can and cannot prove: completeness only relative to an assertion language rich enough to state the invariants. Collects the pursuit of that question from Turing's 1949 assertions through Cook's relative completeness to the higher-order logics where Cook's separation of assertion from specification no longer holds. Membership requires the work to bear on the completeness question itself, not merely to use a program logic.
45 references
Completeness of Iris-Based Program Logics
Johannes Hostert and others (2026) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery (ACM)
Dijkstra's legacy on program verification
Reiner Hähnle (2022) · Edsger Wybe Dijkstra: His Life, Work, and Legacy · Association for Computing Machinery
Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic
Frank S. de Boer and others (2021) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery
Fifty years of Hoare's logic
Krzysztof R. Apt and others (2019) · Formal Aspects of Computing
Completeness of separation logic with inductive definitions for program verification
Makoto Tatsuta and others (2014) · International Conference on Software Engineering and Formal Methods · Springer
Verification of object-oriented programs: A transformational approach
Krzysztof R. Apt and others (2012) · Journal of Computer and System Sciences
Verification of Sequential and Concurrent Programs
Krzysztof R. Apt and others (2009) · Springer
A general framework for sound and complete Floyd-Hoare logics
Rob Arthan and others (2009) · ACM Transactions on Computational Logic · Association for Computing Machinery
Hoare logic in the abstract
Ursula Martin and others (2006) · 20th International Workshop on Computer Science Logic (CSL) · Springer
A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts
Cees Pierik and others (2003) · Formal Methods for Open Object-Based Distributed Systems · Springer
BI as an assertion language for mutable data structures
Samin S. Ishtiaq and others (2001) · 28th ACM Symposium on Principles of Programming Languages (POPL)
Proving pointer programs in Hoare logic
Richard Bornat (2000) · 5th International Conference on Mathematics of Program Construction (MPC) · Springer
A WP-calculus for OO
Frank S. de Boer (1999) · Foundations of Software Science and Computation Structures · Springer
A logic of object-oriented programs
Martín Abadi and others (1997) · TAPSOFT '97: Theory and Practice of Software Development · Springer
Modular Completeness: Integrating the Reuse of Specified Software in Top-down Program Development
Job Zwiers and others (1996) · FME'96: Industrial Benefit and Advances in Formal Methods · Springer
Assigning meanings to programs
Robert W. Floyd (1993) · Program Verification: Fundamental Issues in Computer Science · Springer
Program verification
Nissim Francez (1992) · Addison-Wesley
Reasoning about Dynamically Evolving Process Structures; a proof theory for the parallel object-oriented language pool
Frank S. de Boer (1991) · Vrije Universiteit Amsterdam
The expressive theory of stacks
Samuel Kamin (1987) · Acta Informatica
Some questions about expressiveness and relative completeness in Hoare's logic
Mario Rodriguez Artalejo (1985) · Theoretical Computer Science
On relative completeness of Hoare logics
Michal Grabowski (1985) · Information and Control
Ten Years of Hoare's Logic: A Survey Part II: Nondeterminism
Krzysztof R. Apt (1984) · Theoretical Computer Science
The characterization problem for Hoare logics
Edmund M. Clarke Jr. (1984) · Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences · The Royal Society
Effective axiomatizations of Hoare logics
Edmund M. Clarke Jr. and others (1983) · Journal of the ACM
On the Notion of Expressiveness and the Rule of Adaption
Ernst-Rüdiger Olderog (1983) · Theoretical Computer Science
Expressiveness and the completeness of Hoare's logic
Jan A. Bergstra and others (1982) · Journal of Computer and System Sciences · Elsevier BV
Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
Jan A. Bergstra and others (1982) · Theoretical Computer Science
A General Axiom of Assignment
Joseph M. Morris (1982) · Theoretical Foundations of Programming Methodology · Springer
Ten Years of Hoare's Logic: A Survey - Part I
Krzysztof R. Apt (1981) · ACM Transactions on Programming Languages and Systems
Mathematical theory of program correctness
Jacobus W. de Bakker (1980) · Prentice-Hall
Programming language constructs for which it is impossible to obtain good Hoare axiom systems
Edmund M. Clarke Jr. (1979) · Journal of the ACM
First-Order Dynamic Logic
David Harel (1979) · Springer
Soundness and completeness of an axiom system for program verification
Stephen A. Cook (1978) · SIAM Journal on Computing
A necessary and sufficient condition for the existence of Hoare logics
Richard J. Lipton (1977) · 18th Annual Symposium on Foundations of Computer Science (sfcs 1977) · IEEE
Completeness and incompleteness theorems for Hoare-like axiom systems
Edmund M. Clarke Jr (1976) · Cornell University
An axiomatic proof technique for parallel programs I
Susan Owicki and others (1976) · Acta Informatica · Springer
Verifying properties of parallel programs: An axiomatic approach
Susan Owicki and others (1976) · Communications of the ACM · Association for Computing Machinery (ACM)
Semantical considerations on Floyd-Hoare logic
Vaughan R. Pratt (1976) · 17th Annual Symposium on Foundations of Computer Science · IEEE
On the completeness of the inductive assertion method
Jacobus W. de Bakker and others (1975) · Journal of Computer and System Sciences · Academic Press
An assertion language for data structures
Stephen Cook and others (1975) · Proceedings of the 2nd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '75) · Association for Computing Machinery
A complete axiomatic system for proving assertions about recursive and non-recursive programs
Gerald Arthur Gorelick (1975)
Axiomatic Proof Techniques for Parallel Programs
Susan Speer Owicki (1975) · Cornell University
Procedures and parameters: An axiomatic approach
C. A. R. Hoare (1971) · Symposium on Semantics of Algorithmic Languages
An axiomatic basis for computer programming
C. A. R. Hoare (1969) · Communications of the ACM · Association for Computing Machinery
Assigning meanings to programs
Robert W. Floyd (1967) · Proceedings of symposia in applied mathematics · American Mathematical Society