×

A mechanical analysis of program verification strategies. (English) Zbl 1140.68060

Summary: We analyze three proof strategies commonly used in deductive verification of deterministic sequential programs formalized with operational semantics. The strategies are (i) stepwise invariants, (ii) clock functions, and (iii) inductive assertions. We show how to formalize the strategies in the logic of the ACL2 theorem prover. Based on our formalization, 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. The soundness and completeness theorems have been mechanically checked with ACL2.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Apt, K.R.: Ten years of Hoare’s logic: a survey – Part I. ACM Trans. Program. Lang. Syst. (ACM TOPLAS) 3(4), 431–483 (1981) · Zbl 0471.68006 · doi:10.1145/357146.357150
[2] Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)
[3] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, New York (2004) · Zbl 1069.68095
[4] Bevier, W.R.: A Verified Operating System Kernel. Ph.D. thesis, Department of Computer Sciences, The University of Texas at Austin (1987)
[5] Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D.: An approach to system verification. J. Autom. Reason. 5(4), 411–428 (1989)
[6] Boyer, R.S., Goldshlag, D., Kaufmann, M., Moore, J.S.: Functional instantiation in first order logic. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 7–26. Academic, London (1991) · Zbl 0755.68120
[7] Boyer, R.S., Kaufmann, M., Moore, J.S.: The Boyer-Moore theorem prover and its interactive enhancement. Comput. Math. Appl. 29(2), 27–62 (1995) · Zbl 00718810 · doi:10.1016/0898-1221(94)00215-7
[8] Boyer, R.S., Moore, J.S.: A Computational Logic. Academic, New York (1979) · Zbl 0448.68020
[9] Boyer, R.S., Moore, J.S.: Mechanized formal reasoning about programs and computing machines. In: Veroff, R. (ed.) Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pp. 141–176. MIT, Cambridge (1996)
[10] Brock, B., Hunt, Jr., W.A.: Formal analysis of the Motorola CAP DSP. In: Hinchey M.G., Bowen J.P. (eds.) Industrial-Strength Formal Methods. Springer, New York (1999)
[11] Church, A., Kleene, S.C.: Formal definitions in the theory of ordinal numbers. Fundam. Math. 28, 11–21 (1937) · Zbl 0016.00201
[12] Clarke, E.M.: Completeness and Incompleteness of Hoare-like Axiom Systems. Ph.D. thesis, Cornell University (1976)
[13] Clint, M.: Program proving: coroutines. Acta Inform. 2, 50–63 (1973) · doi:10.1007/BF00571463
[14] Clint, M., Hoare, C.A.R.: Program proving: jumps and functions. Acta Inform. 1, 214–224 (1971) · Zbl 0229.68003 · doi:10.1007/BF00288686
[15] Colby, C., Lee, P., Necula, G.C., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI 2000), pp. 95–107, Vancouver, British Columbia, 18–21 June 2000
[16] Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70–90 (1978) · Zbl 0374.68009 · doi:10.1137/0207005
[17] de Bakker, J.W.: Mathematical Theory of Program Correctness. Prentice-Hall, Englewood Cliffs (1980) · Zbl 0452.68011
[18] Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking for java. Technical Report 159, Compaq Systems Research Center (1998)
[19] Dijkstra, E.W.: Guarded commands, non-determinacy and a calculus for derivation of programs. In: Bauer, F.L., Samelson, K. (eds.) Language Hierarchies and Interfaces, pp. 111–124. Springer, New York (1975)
[20] Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1978) · Zbl 0397.68010
[21] Flatau, A.D.: A Verified Language Implementation of an Applicative Language with Dynamic Storage Allocation. Ph.D. thesis, Department of Computer Sciences, The University of Texas at Austin (1992)
[22] Floyd, R.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society, Providence (1967) · Zbl 0189.50204
[23] Fox, A.C.J.: Formal specification and verification of ARM6. In: Basin, D.A., Wolff, B. (eds.) Proceedings of the 16th International Conference on Theorem Proving in Higher-Order Logics (TPHOLS 2003), LNCS, vol. 2758, pp. 25–40, Rome, 8–12 September 2003
[24] Gloess, P.Y.: Imperative Program Verification in PVS. Technical report, École Nationale Supérieure Électronique, Informatique et Radiocommunications de bordeaux. See URL http://www.labri.fr/perso/gloess/imperative (1999)
[25] Goldstein, H.H., von Neumann, J.: Planning and coding problems for an electronic computing instrument. In: Taub, A.H. (ed.) John von Neumann, Collected Works, vol. 5. Pergamon, Oxford (1961)
[26] Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993) · Zbl 0779.68007
[27] Greve, D., Wilding, M., Hardin, D.: High-speed, analyzable simulators. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, pp. 89–106. Springer, Boston (2000)
[28] Hamon, G., Rushby, J.: An operational semantics for stateflow. In: Wermelinger, M., Margaria, T. (eds.) Proceedings of the 7th International Conference on Fundamental Approaches to Software Engineering (FASE 2004). LNCS, vol. 2984, pp. 229–243. Springer, New York (2004) · Zbl 1129.68445
[29] Harrison, J.: Formalizing Dijkstra. In: Grundy, J., Newer, M. (eds.) Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 1998). LNCS, vol. 1479, pp. 171–188. Springer, New York (1998)
[30] Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–583 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[31] Hoare, C.A.R.: Proof of correctness of data representations. Acta Inform. 1, 271–281 (1972) · Zbl 0244.68009 · doi:10.1007/BF00289507
[32] Homeier, P., Martin, D.: A mechanically verified verification condition generator. Comput. J. 38(2), 131–141 (1995) · Zbl 05479913 · doi:10.1093/comjnl/38.2.131
[33] Hunt Jr., W.A.: FM8501: A Verified Microprocessor. LNAI, vol. 795. Springer, New York (1994)
[34] Hunt Jr., W.A., Brock, B.: A formal HDL and its use in the FM9001 verification. In: Hoare, C.A.R., Gordon, M.J.C. (eds.) Mechanized Reasoning and Hardware Design, pp. 35–48. Prentice Hall, Englewood Cliffs (1992)
[35] Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Boston (2000)
[36] Kaufmann, M., Moore, J.S.: ACL2 home page. See URL http://www.cs.utexas.edu/users/moore/acl2 (2006)
[37] King, J.C.: A Program Verifier. Ph.D. thesis, Carnegie-Melon University (1969) · Zbl 0255.68005
[38] King, S., Hammond, J., Chapman, R., Pryor, A.: Is proof more cost-effective than testing? IEEE Trans. Softw. Eng. 26(8), 675–686 (2000) · Zbl 05114162 · doi:10.1109/32.879807
[39] Liu, H., Moore, J.S.: Java program verification via a JVM deep embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), Park City. LNCS, vol. 3233, pp. 184–200. Springer, New York (2004) · Zbl 1099.68731
[40] Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: a study. Sci. Comput. Program. 57(3), 253–274 (2005) · Zbl 1077.68560 · doi:10.1016/j.scico.2004.07.004
[41] Manna, Z.: The correctness of programs. J. Comput. Syst. Sci. 3(2), 119–127 (1969) · Zbl 0285.68011 · doi:10.1016/S0022-0000(69)80009-7
[42] Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995) · Zbl 0844.68079
[43] Manolios, P., Moore, J.S.: Partial functions in ACL2. J. Autom. Reason. 31(2), 107–127 (2003) · Zbl 1060.68109 · doi:10.1023/B:JARS.0000009505.07087.34
[44] Manolios, P., Vroon, D.: Algorithms for ordinal arithmetic. In: Baader, F. (ed.) Proceedings of the 19th International Conference on Automated Deduction (CADE 2003). Miami LNAI, vol. 2741, pp. 243–257. Springer, New York (2003) · Zbl 1278.68272
[45] Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition deneration via theorem proving. In: Hermann, M., Voronkov, A. (eds.) Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006). LNCS, vol. 4246, pp. 362–376. Springer, New York (2006) · Zbl 1165.68410
[46] Matthews, J., Vroon, D.: Partial clock functions in ACL2. In: Kaufmann, M., Moore, J.S. (eds.) 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004). Austin, TX, 18–19 November 2004
[47] McCarthy, J.: Towards a mathematical science of computation. In: Proceedings of the Information Processing Congress, vol. 62, pp. 21–28, Munich, 27 August–1 September 1962
[48] Mehta, F., Nipkow, T.: Proving pointer programs in higher order logic. In: Baader, F. (ed.) Proceedings of the 19th International Conference on Automated Deduction (CADE 2003). LNAI, vol. 2741, pp. 121–135. Springer, New York (2003) · Zbl 1278.68274
[49] Moore, J.S.: Piton: A Mechanically Verified Assembly Language. Kluwer, Boston (1996)
[50] Moore, J.S.: Inductive assertions and operational semantics. In: Geist, D. (ed.) Proceedings of the 12th International Conference on Correct Hardware Design and Verification Methods. LNCS, vol. 2860, pp. 289–303. Springer, New York (2003) · Zbl 1179.68089
[51] Moore, J.S.: Proving theorems about java and the JVM with ACL2. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logic of Engineering Software, pp. 227–290. IOS, Amsterdam (2003)
[52] Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997), pp. 106–119, Paris, 15–17 January 1997
[53] Norrish, M.: C Formalised in HOL. Ph.D. thesis, University of Cambridge (1998)
[54] Oppen, D.C., Cook, S.A.: Proving assertions about programs that manipulate data structures. In: Proceedings of the 7th Annual ACM Symposium on Theory of Computing (STOC 1975), pp. 107–116, Albuquerque, 5–7 May 1975 · Zbl 0359.68011
[55] Ortner, V., Schirmer, N.: Verification of BDD normalization. In: Hurd, J., Melham, T. (eds.) Proceedings of the 16th International Conference on Theorem Proving in Higher-Order Logics (TPHOLS 2005). LNCS, vol. 3603, pp. 261–277. Springer, New York (2005) · Zbl 1152.68532
[56] Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279–285 (1976) · Zbl 0322.68010 · doi:10.1145/360051.360224
[57] Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapoor, D. (ed.) 11th International Conference on Automated Deduction (CADE). LNAI, vol. 607, pp. 748–752. Springer, New York (1992)
[58] Ray, S., Hunt Jr., W.A.: Deductive verification of pipelined machines using first-order quantification. In: Alur, R., Peled, D.A. (eds.) Proceedings of the 16th International Conference on Computer-Aided Verification (CAV 2004). Boston, MA LNCS, vol. 3114, pp. 31–43. Springer, New York (2004) · Zbl 1103.68634
[59] Ray, S., Moore, J.S.: Proof styles in operational semantics. In: Hu, A.J., Martin, A.K. (eds.) Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004). Austin, TX LNCS, vol. 3312, pp. 67–81. Springer, New York (2004) · Zbl 1117.68419
[60] Sawada, J., Hunt Jr., W.A.: Trace table based approach for pipelined microprocessor verification. In: Grumberg, O. (ed.) Proceedings of the 9th International Conference on Computer-Aided Verification (CAV 1997). LNCS, vol. 1254, pp. 364–375. Springer, New York (1997)
[61] Schirmer, N.: A verification environment for sequential imperative programs in Isabelle/HOL. In: Baader, F., Voronkov, A. (eds.) Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004). LNAI, vol. 3452, pp. 398–414. Springer, New York (2005) · Zbl 1108.68410
[62] Shankar, N.: Machine-assisted verification using theorem proving and model checking. In: Broy, M., Schieder, B. (eds.) Mathematical Methods in Program Development. NATO ASI Series F: Computer and Systems Science, vol. 158, pp. 499–528. Springer, New York (1997) · Zbl 0884.68115
[63] Sokolowski, S.: Axioms for total correctness. Acta Inform. 9, 61–71 (1977) · Zbl 0363.68011 · doi:10.1007/BF00263765
[64] Strecker, M.: Formal verification of a Java compiler in Isabelle. In: Voronkov, A. (ed.) Proeedings of the 18th International Conference on Automated Deduction (CADE 2002). LNCS, vol. 2392, pp. 63–77. Springer, New York (2002) · Zbl 1072.68593
[65] Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machine, pp. 67–69. University Mathematical Laboratory, Cambridge (1949)
[66] Wand, M.: A new incompleteness result for Hoare’s system. J. ACM 25(1), 168–175 (1978) · Zbl 0364.68008 · doi:10.1145/322047.322062
[67] Wilding, M.: A mechanically verified application for a mechanically verified environment. In: Courcoubetis, C. (ed.) Proceedings of the 5th International Conference on Computer-Aided Verification (CAV 1993). LNCS, vol. 697, pp. 268–279. Springer, New York (1993)
[68] Wilding, M.: Robust computer system proofs in PVS. In: Holloway, C.M., Hayhurst, K.J. (eds.) 4th NASA Langley Formal Methods Workshop. NASA, Washington, DC (1997)
[69] Young, W.D.: A verified code generator for a subset of Gypsy. Technical Report 33, Computational Logic Inc (1988)
[70] Yu, Y.: Automated Proofs of Object Code for a Widely Used Microprocessor. Ph.D. thesis, Department of Computer Sciences, The University of Texas at Austin (1992) · Zbl 0882.68128
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.