OpenSkillIndex← back to search
claude-codescience

Babysitter termination-analyzer

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

install
source · Clone the upstream repo
git clone https://github.com/a5c-ai/babysitter
Claude Code · Install into ~/.claude/skills/
T=$(mktemp -d) && git clone --depth=1 https://github.com/a5c-ai/babysitter "$T" && mkdir -p ~/.claude/skills && cp -r "$T/library/specializations/domains/science/computer-science/skills/termination-analyzer" ~/.claude/skills/a5c-ai-babysitter-termination-analyzer && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/termination-analyzer/SKILL.md
tags
#algorithm-analysis#termination-proof#ranking-functions#formal-verification#logic-proving
source content

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