A note on the complexity of propositional Hoare logic

ABSTRACT

We provide a simpler alternative proof of the PSPACE-hardness of propositional Hoare logic (PHL).

REFERENCES

• 1: Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981 [doi>10.1145/357146.357150]
• 2: Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
• 3: Dexter Kozen, On Hoare logic and Kleene algebra with tests, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.60-76, July 2000 [doi>10.1145/343369.343378]
• 4: KOZEN, D. AND TIURYN, J. 2000. On the completeness of propositional Hoare logic. In Proceedings of the 5th International Seminar on Relational Methods in Computer Science (RelMicCS, Jan.), J. Desharnais, Ed. 195-202.
• 5: Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem, Carnegie Mellon University, Pittsburgh, PA, 1992

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Structured programming**
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification; Pre- and post-conditions; Logics of programs; Invariants; Specification techniques; Assertions
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

General Terms:
Design, Theory, Verification

Keywords:
Hoare logic, specification