Agent-Skills.md

Agent Skills: Counterexample-Guided Refinement

Implement CEGAR for synthesis and verification workflows

program-synthesisID: a5c-ai/babysitter/counterexample-guided-refinement

Repository

a5c-ai/babysitter
a5c-aiLicense: MIT
244

Install this agent skill to your local

pnpm dlx add-skill https://github.com/a5c-ai/babysitter/tree/HEAD/plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/counterexample-guided-refinement

Skill Files

Browse the full folder contents for counterexample-guided-refinement.

Download Skill

Loading file tree…

plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/counterexample-guided-refinement/SKILL.md

Skill Metadata

Name
counterexample-guided-refinement
Description
Implement CEGAR for synthesis and verification workflows

Counterexample-Guided Refinement

Purpose

Provides expert guidance on CEGAR (Counterexample-Guided Abstraction Refinement) for verification and synthesis.

Capabilities

  • Counterexample analysis
  • Predicate abstraction refinement
  • Interpolation-based refinement
  • Abstraction refinement loop management
  • Convergence analysis
  • Spurious counterexample detection

Usage Guidelines

  1. Initial Abstraction: Define initial abstraction
  2. Verification: Check abstract model
  3. Counterexample Analysis: Analyze counterexamples
  4. Refinement: Refine abstraction if spurious
  5. Iteration: Repeat until verified or real counterexample

Tools/Libraries

  • CPAChecker
  • SeaHorn
  • BLAST
  • SLAM