Certified Size-Change Termination

14 years 4 months ago

Download www4.in.tum.de

We develop a formalization of the Size-Change Principle in Isabelle/HOL and use it to construct formally certified termination proofs for recursive functions automatically.

Alexander Krauss

Real-time Traffic

Automated Reasoning | CADE 2007 | Termination Proofs |

claim paper

Related Content

» Lazy Abstraction for SizeChange Termination

» SizeChange Termination Monotonicity Constraints and Ranking Functions

» Covered Clause Elimination

» Certified Subterm Criterion and Certified Usable Rules

» A3PAT an approach for certified automated termination proofs

» On Tree Automata that Certify Termination of LeftLinear Term Rewriting Systems

» Certifying a Termination Criterion Based on Graphs without Graphs

» Interactive Termination Proofs Using Termination Cores

» Finding and Certifying Loops

Post Info
More Details (n/a)

Added	03 Dec 2009
Updated	03 Dec 2009
Type	Conference
Year	2007
Where	CADE
Authors	Alexander Krauss

Comments (0)

Sciweavers

Certified Size-Change Termination

Automated Reasoning | CADE 2007 | Termination Proofs |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers