Abstract
Termination poses one of the main challenges for mechanically verifying infinite state systems. In this paper, we develop a powerful and extensible framework based on the ordinals for reasoning about termination in a general purpose programming language. We have incorporated our work into the ACL2 theorem proving system, thereby greatly extending its ability to automatically reason about termination. The resulting technology has been adopted into the newly released ACL2 version 2.8. We discuss the creation of this technology and present two case studies illustrating its effectiveness.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Boyer, R.S., Moore, J.S.: Proving theorems about pure lisp functions. JACM 22(1), 129–144 (1975)
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979)
Colón, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67–81. Springer, Heidelberg (2001)
Colón, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002)
Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Workshop on Advanced Verification (July 2000), See http://www.cs.utah.edu/wave/
Hirokawa, N., Middledorp, A.: Automating the dependency pair method. In: Automated Deduction – CADE-19. LNCS (LNAI), pp. 32–46. Springer, Heidelberg (2003)
Hu, A.J., Vardi, M.Y. (eds.): Computer-Aided Verification – CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Moore, J.S.: ACL2 homepage. See, http://www.cs.utexas.edu/users/moore/acl2
Kaufmann, M., Moore, J.S. (eds.): Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003) (July 2003), See http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. ACM Symposium on Principles of Programming Languages 28, 81–92 (2001)
Manolios, P., Vroon, D.: Algorithms for ordinal arithmetic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 243–257. Springer, Heidelberg (2003)
Manolios, P., Vroon, D.: Ordinal arithmetic in ACL2. In: Kaufmann and Moore [13], See http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/
Martín-Mateos, F.-J., Alonso, J.-A., Hidalgo, M.-J., Ruiz-Reina, J.-L.: A formal proof of Dickson’s Lemma in ACL2. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 49–58. Springer, Heidelberg (2003)
Morris, F., Jones, C.: An early program proof by Alan Turing. IEEE Annals of the History of Computing 6(2), 139–143 (1984)
Podelske, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Ruiz-Reina, J.-L., Alonso, J.-A., Hidalgo, M.-J., Martin, F.-J.: Multiset relations: A tool for proving termination. In: Kaufmann, M., Moore, J.S. (eds.) Proceedings of the ACL2 Workshop 2000. The University of Texas at Austin, Technical Report TR-00-29 (November 2000)
Sustik, M.: Proof of Dixon’s lemma using the ACL2 theorem prover via an explicit ordinal mapping. In: Kaufmann and Moore [13], See http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/
Wilding, M., Greve, D., Hardin, D.: Efficient simulation of formal processor models. Formal Methods in System Design 18(3), 233–248 (2001)
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
Manolios, P., Vroon, D. (2004). Integrating Reasoning About Ordinal Arithmetic into ACL2. 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_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-30494-4_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23738-9
Online ISBN: 978-3-540-30494-4
eBook Packages: Springer Book Archive