Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

12

FMCAD
2004
Springer

favoriteEmaildiscussreport

97views Formal Methods» more FMCAD 2004»

Integrating Reasoning About Ordinal Arithmetic into ACL2

13 years 9 months ago

Integrating Reasoning About Ordinal Arithmetic into ACL2

Download www.ccs.neu.edu

Abstract. Termination poses one of the main challenges for mechanically verifying inﬁnite 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

Real-time Traffic

FMCAD 2004 | Inﬁnite State Systems | Purpose Programming Language | Theorem Proving System |

claim paper

Related Content

» Algorithms for Ordinal Arithmetic

» Parameterized congruences in ACL2

» An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving

» Proofs Programs and Abstract Complexity

» Formal Reasoning about Expectation Properties for Continuous Random Variables

» Separation logic superposition calculus heap theorem prover

» CSIsat Interpolation for LAEUF

» Complete Functional Synthesis

» Efficient state space exploration Interleaving stateless and statebased model checking

Post Info
More Details (n/a)

Added	01 Jul 2010
Updated	01 Jul 2010
Type	Conference
Year	2004
Where	FMCAD
Authors	Panagiotis Manolios, Daron Vroon

Comments (0)