Verification

This section documents the verification tools and frameworks used throughout Lotus.

• Verification Support Analyses
• Verification Backend API
• CLAM – Abstract Interpretation Framework
  • Overview
  • Components
  • Build Targets
  • Usage
  • Programmatic Usage
  • Abstract Domains
  • Integration Points
  • See Also
• Sifa
  • Overview
  • Main components
  • Domain choices
  • Typical usage
  • See also
• SymAbsAI – Symbolic Abstraction + Abstract Interpretation
• SeaHorn Verification Framework
  • Overview
  • Structure
  • Components
  • SeaHorn Verification
• Failure-Directed Trimming
  • Overview
  • Use cases
  • Notes
• Verification Transformation Passes