Abstract
abs We relate two well-studied methodologies in deductive verification of operationally modeled sequential programs, namely the use of inductive invariants and clock functions. We show that the two methodologies are equivalent and one can mechanically transform a proof of a program in one methodology to a proof in the other. Both partial and total correctness are considered. This mechanical transformation is compositional; different parts of a program can be verified using different methodologies to achieve a complete proof of the entire program. The equivalence theorems have been mechanically checked by the ACL2 theorem prover and we implement automatic tools to carry out the transformation between the two methodologies in ACL2.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
McCarthy, J.: Towards a Mathematical Science of Computation. In: Proceedings of the Information Processing Congress, vol. 62, pp. 21–28. North-Holland, Amsterdam (1962)
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 Press, Cambridge (1996)
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 Press, Amsterdam (2003)
Bevier, W.R.: A Verified Operating System Kernel. PhD thesis, Department of Computer Sciences, The University of Texas at Austin (1987)
Young, W.D.: A Verified Code Generator for a Subset of Gypsy. Technical Report 33, Computational Logic Inc (1988)
Flatau, A.D.: A Verified Implementation of an Applicative Language with Dynamic Storage Allocation. PhD thesis (1992)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Moore, J.S.: Structured Theory Development for a Mechanized Logic. Journal of Automated Reasoning 26, 161–203 (2001)
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1975)
Liu, H., Moore, J.S.: Executable JVM Model for Analytical Reasoning: A Study. In: ACM SIGPLAN 2003 Workshop on Interpreters, Virtual Machines, and Emulators, San Diego, CA (2003)
Wilding, M.: Robust Computer System Proofs in PVS. In: Holloway, C.M., Hayhurst, K.J. (eds.) Fourth NASA Langley Formal Methods Workshop. NASA Conference Publication, vol. 3356 (1997)
Floyd, R.: Assigning Meanings to Programs. In: Proceedings of Symposia in Applied Mathematcs. Mathematical Aspects of Computer Science, vol. XIX, pp. 19–32. American Mathematical Society, Providence, Rhode Island (1967)
Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12, 576–583 (1969)
Dijkstra, E.W.: Guarded Commands, Non-determinacy and a Calculus for Derivation of Programs. Language Hierarchies and Interfaces, 111–124 (1975)
Moore, J.S.: Inductive Assertions and Operational Semantics. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 289–303. Springer, Heidelberg (2003)
Ray, S., Hunt Jr., W.A.: Deductive Verification of Pipelined Machines Using First-Order Quantification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 31–43. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ray, S., Moore, J.S. (2004). Proof Styles in Operational Semantics. In: Hu, A.J., Martin, A.K. (eds) Formal Methods in Computer-Aided Design. FMCAD 2004. Lecture Notes in Computer Science, vol 3312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30494-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-30494-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23738-9
Online ISBN: 978-3-540-30494-4
eBook Packages: Springer Book Archive