Integrating Reasoning About Ordinal Arithmetic into ACL2

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.

• Type: Conference
• Year: 2004
• Where: FMCAD
• Authors: Panagiotis Manolios, Daron Vroon
• Keywords: FMCAD 2004, Infinite State Systems, Purpose Programming Language, Theorem Proving System