Termination Analyzer

Prove termination of algorithms and programs using ranking functions and well-founded orderings

a5c-ai Updated 1.7k repo stars

File contents

Termination Analyzer

Purpose

Provides expert guidance on proving termination of algorithms through ranking functions, well-founded orderings, and automated analysis.

Capabilities

  • Identify ranking/variant functions automatically
  • Prove well-founded orderings
  • Handle mutual recursion
  • Detect potential non-termination
  • Generate termination certificates
  • Analyze complex control flow

Usage Guidelines

  1. Structure Analysis: Identify recursive calls and loop structures
  2. Ranking Function: Find or construct appropriate ranking function
  3. Ordering Proof: Prove well-foundedness of the ordering
  4. Certificate Generation: Generate formal termination proof
  5. Non-termination Detection: Flag potential infinite loops

Tools/Libraries

  • AProVE
  • T2
  • Ultimate Automizer
  • SMT solvers

a5c-ai/babysitter/tree/main/library/specializations/domains/science/computer-science/skills/termination-analyzer commit 7b52a81fd2

Frequently asked questions

npx skillmds@latest add a5c-ai/termination-analyzer