Integrating Reasoning about Ordinal Arithmetic into ACL2

---

Panagiotis Manolios and Daron Vroon.
FMCAD 2004, Formal Methods in Computer-Aided Design. © Springer-Verlag

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.

PDF (167K) © Springer-Verlag
Postscript (201K) © Springer-Verlag