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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
One notable exception is the Hoare logic. There has been significant work on analysis of soundness and completeness of Hoare axioms for various programming language constructs. See the bibliographic notes for this chapter.
- 2.
This criticism has been rarely written in print, but usually expressed in conference question–answer sessions. However, there has been a nagging feeling that clock functions require more work. The absence of published criticism and the presence of this “nagging feeling” have both been confirmed by an extensive literature search and private communications with some of the authors of other theorem provers.
- 3.
The actual symbol they use is \(\mathtt{=\,=}\) instead of ↪. We use the latter to avoid confusion between this relation and equality.
References
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.
W. R. Bevier. A Verified Operating System Kernel. PhD thesis, Department of Computer Sciences, The University of Texas at Austin, 1987.
R. S. Boyer and Y. Yu. Automated Proofs of Object Code for a Widely Used Microprocessor. Journal of the ACM, 43(1), January 1996.
E. M. Clarke. Completeness and Incompleteness of Hoare-Like Axiom Systems. PhD thesis, Cornell University, 1976.
M. Clint. Program Proving: Coroutines. Acta Informatica, 2:50–63, 1973.
M. Clint and C. A. R. Hoare. Program Proving: Jumps and Functions. Acta Informatica, 1:214–224, 1971.
S. A. Cook. Soundness and Completeness of an Axiom System for Program Verification. SIAM Journal of Computing, 7(1):70–90, 1978.
J. W. de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall, 1980.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1978.
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.
C. A. R. Hoare. Proof of Correctness of Data Representations. Acta Informatica, 1:271–281, 1972.
W. A. Hunt, Jr. FM8501: A Verified Microprocessor, volume 795 of LNAI. Springer-Verlag, 1994.
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.
P. Manolios and J. S. Moore. Partial Functions in ACL2. Journal of Automated Reasoning, 31(2):107–127, 2003.
J. S. Moore. Piton: A Mechanically Verified Assembly Language. Kluwer Academic Publishers, 1996.
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.
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.
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.
S. S. Owicki and D. Gries. Verifying Properties of Parallel Programs: An Axiomatic Approach. Communications of the ACM, 19(5):279–285, 1976.
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.
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.
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.
S. Sokolowski. Axioms for Total Correctness. Acta Informatica, 9:61–71, 1977.
M. Wand. A New Incompleteness Result for Hoare’s System. Journal of the ACM, 25(1): 168–175, January 1978.
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.
W. D. Young. A Verified Code Generator for a Subset of Gypsy. Technical Report 33, Computational Logic Inc., 1988.
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.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Ray, S. (2010). Connecting Different Proof Styles. In: Scalable Techniques for Formal Verification. Springer, Boston, MA. https://doi.org/10.1007/978-1-4419-5998-0_6
Download citation
DOI: https://doi.org/10.1007/978-1-4419-5998-0_6
Published:
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-5997-3
Online ISBN: 978-1-4419-5998-0
eBook Packages: EngineeringEngineering (R0)