Integrating Reasoning about Ordinal Arithmetic into ACL2
Panagiotis Manolios and Daron Vroon.
FMCAD 2004, Formal Methods in Computer-Aided Design. © Springer-Verlag
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