Sciweavers

Share
FMCAD
2004
Springer

Integrating Reasoning About Ordinal Arithmetic into ACL2

9 years 3 months ago
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.
Panagiotis Manolios, Daron Vroon
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where FMCAD
Authors Panagiotis Manolios, Daron Vroon
Comments (0)
books