Verification

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

• Verification Support Analyses
• Verification Backend API
• CRAB - Abstract Interpretation Library
  • Overview
  • Repository Structure
  • Build Configuration
  • Integration With Lotus
  • See Also
• CLAM – Abstract Interpretation Framework
  • Overview
  • Components
  • Build Targets
  • Usage
  • Programmatic Usage
  • Abstract Domains
  • Integration Points
  • See Also
• SMACK Verification Frontend
  • Copied Documentation
  • Build Targets
  • See Also
• Sifa
  • Overview
  • Main components
  • Domain choices
  • Typical usage
  • See also
• Seal — Symbolic Automata for Stateful Systems
  • Overview
  • Directory Structure
  • Build
  • Usage
• SymAbsAI – Symbolic Abstraction + Abstract Interpretation
• SeaHorn Verification Framework
  • Overview
  • Structure
  • Components
  • SeaHorn Verification
• Failure-Directed Trimming
  • Overview
  • Use cases
  • Notes
• Verification Frontend
  • BooleanProgram
• Verification Transformation Passes