CLI and Tools

• CLI Tools
  • Registered console scripts
  • Quick start
  • Tool summaries
  • Validation
• Translator Module
  • Current scope
  • Programmatic usage
  • CLI access
  • Notes
• Applications
  • Testing
  • Verification
  • Synthesis
  • Optimization
  • Learning & AI
• Boogie Frontend for EFMC
  • Overview
  • Usage
  • Supported Boogie Features
  • Example Boogie Programs
  • Verification Workflow
  • Generated Transition System
  • Integration with EFMC Engines
  • CHC Format Generation
  • Limitations
  • Future Enhancements
  • Error Handling
  • Testing
• C Frontend for EFMC
  • Overview
  • Usage
  • Supported C Features
  • Limitations
  • Example C Programs
  • Verification Workflow
  • Generated Transition System
  • Integration with EFMC Engines
  • CHC Format Generation
  • Command-Line Usage
  • Future Enhancements
  • Error Handling
  • Testing
• Constrained Horn Clauses (CHC) Tools
  • Introduction
  • Core Components
  • CHC Parser
  • Horn Database
  • CHC Solver
  • Model Validation
  • Pretty Printer
  • Advanced Features
  • Integration Examples
  • Command-Line Tools
  • Related Work and References
• Verification Tools
  • Architecture
  • Common Utilities
  • Boogie Frontend Tools
  • Verification Condition Generation
  • Daikon Integration
  • CPAchecker Integration
  • ICE-based Invariant Generation
  • API Reference