Connecting Different Proof Styles

Chapter

Abstract

We consider formal relation between the three common program verification strategies. In particular, we prove that each strategy is both sound and complete. The completeness result implies that given any proof of correctness of a sequential program one can derive a proof in each of the above strategies.

Keywords

Hunt Encapsulation 

References

  1. 5.
    K. R. Apt. Ten Years of Hoare’s Logic: A Survey – Part I. ACM Transactions on Programming Languages and Systems (ACM TOPLAS), 3(4):431–483, October 1981.MATHCrossRefGoogle Scholar
  2. 14.
    W. R. Bevier. A Verified Operating System Kernel. PhD thesis, Department of Computer Sciences, The University of Texas at Austin, 1987.Google Scholar
  3. 27.
    R. S. Boyer and Y. Yu. Automated Proofs of Object Code for a Widely Used Microprocessor. Journal of the ACM, 43(1), January 1996.Google Scholar
  4. 48.
    E. M. Clarke. Completeness and Incompleteness of Hoare-Like Axiom Systems. PhD thesis, Cornell University, 1976.Google Scholar
  5. 55.
    M. Clint. Program Proving: Coroutines. Acta Informatica, 2:50–63, 1973.CrossRefGoogle Scholar
  6. 56.
    M. Clint and C. A. R. Hoare. Program Proving: Jumps and Functions. Acta Informatica, 1:214–224, 1971.MATHCrossRefGoogle Scholar
  7. 60.
    S. A. Cook. Soundness and Completeness of an Axiom System for Program Verification. SIAM Journal of Computing, 7(1):70–90, 1978.MATHCrossRefGoogle Scholar
  8. 64.
    J. W. de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall, 1980.Google Scholar
  9. 68.
    E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1978.Google Scholar
  10. 99.
    J. Harrison. Formalizing Dijkstra. In J. Grundy and M. Newer, editors, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 1998), volume 1479 of LNCS, pages 171–188, Canberra, ACT, 1998, Springer-Verlag.CrossRefGoogle Scholar
  11. 104.
    C. A. R. Hoare. Proof of Correctness of Data Representations. Acta Informatica, 1:271–281, 1972.MATHCrossRefGoogle Scholar
  12. 108.
    W. A. Hunt, Jr. FM8501: A Verified Microprocessor, volume 795 of LNAI. Springer-Verlag, 1994.Google Scholar
  13. 147.
    H. Liu and J. S. Moore. Java Program Verification via a JVM Deep Embedding in ACL2. In K. Slind, A. Bunker, and G. Gopalakrishnan, editors, Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), volume 3233 of LNCS, pages 184–200, Park City, Utah, 2004. Springer-Verlag.CrossRefGoogle Scholar
  14. 153.
    P. Manolios and J. S. Moore. Partial Functions in ACL2. Journal of Automated Reasoning, 31(2):107–127, 2003.MathSciNetMATHCrossRefGoogle Scholar
  15. 173.
    J. S. Moore. Piton: A Mechanically Verified Assembly Language. Kluwer Academic Publishers, 1996.Google Scholar
  16. 175.
    J. S. Moore. Proving Theorems About Java-Like Byte Code. In E. R. Olderog and B. Stefen, editors, Correct System Design – Recent Insights and Advances, volume 1710 of LNCS, pages 139–162, 1999.Google Scholar
  17. 178.
    J. S. Moore. Proving Theorems About Java and the JVM with ACL2. In M. Broy and M. Pizka, editors, Models, Algebras, and Logic of Engineering Software, pages 227–290. IOS Press, 2003.Google Scholar
  18. 192.
    D. C. Oppen and S. A. Cook. Proving Assertions About Programs that Manipulate Data Structures. In Proceedings of the 7th Annual ACM Symposium on Theory of Computing (STOC 1975), pages 107–116, Albuquerque, NM, 1975. ACM Press.Google Scholar
  19. 193.
    S. S. Owicki and D. Gries. Verifying Properties of Parallel Programs: An Axiomatic Approach. Communications of the ACM, 19(5):279–285, 1976.MathSciNetMATHCrossRefGoogle Scholar
  20. 210.
    S. Ray and W. A. Hunt, Jr. Deductive Verification of Pipelined Machines Using First-Order Quantification. In R. Alur and D. A. Peled, editors, Proceedings of the 16th International Conference on Computer-Aided Verification (CAV 2004), volume 3114 of LNCS, pages 31–43, Boston, MA, July 2004. Springer-Verlag.CrossRefGoogle Scholar
  21. 211.
    S. Ray, W. A. Hunt, Jr., J. Matthews, and J. S. Moore. A Mechanical Analysis of Program Verification Strategies. Journal of Automated Reasoning, 40(4):245–269, May 2008.MathSciNetMATHCrossRefGoogle Scholar
  22. 213.
    S. Ray and J. S. Moore. Proof Styles in Operational Semantics. In A. J. Hu and A. K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004), volume 3312 of LNCS, pages 67–81, Austin, TX, November 2004. Springer-Verlag.Google Scholar
  23. 240.
    S. Sokolowski. Axioms for Total Correctness. Acta Informatica, 9:61–71, 1977.MathSciNetMATHCrossRefGoogle Scholar
  24. 254.
    M. Wand. A New Incompleteness Result for Hoare’s System. Journal of the ACM, 25(1): 168–175, January 1978.MathSciNetMATHCrossRefGoogle Scholar
  25. 258.
    M. Wilding. Robust Computer System Proofs in PVS. In C. M. Holloway and K. J. Hayhurst, editors, 4th NASA Langley Formal Methods Workshop, number 3356 in NASA Conference Publication, 1997.Google Scholar
  26. 260.
    W. D. Young. A Verified Code Generator for a Subset of Gypsy. Technical Report 33, Computational Logic Inc., 1988.Google Scholar
  27. 261.
    Y. Yu. Automated Proofs of Object Code for a Widely Used Microprocessor. PhD thesis, Department of Computer Sciences, The University of Texas at Austin, 1992.Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  1. 1.Department of Computer SciencesUniversity of Texas, AustinAustinUSA

Personalised recommendations