Verification

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

• Verification Support Analyses
  • Pipeline use
• Nested Word Automata
  • Semantics and ownership
  • Basic usage
  • Difference and determinization
  • Search and liveness
  • Reduction and incremental inclusion
  • Memory and cancellation
  • Verification
  • Algorithm references
• Trace Abstraction
  • Usage
  • Unified transition formulas and integer arithmetic
  • Memory and procedure state
  • Nested proofs and generalization
  • Current boundaries
  • Tests and Ultimate references
• Verification Backend API
  • Backend lifecycle
• 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
• Mosaic
  • Overview
  • Key Components
  • Usage
• SMACK Verification Frontend
  • Upstream documentation
  • Build Targets
  • See Also
• Sifa
  • Overview
  • Main components
  • Domain choices
  • Typical usage
  • Selecting an abstraction
  • 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
  • Integration considerations
• Verification Frontend
  • BooleanProgram
  • Scope and usage
• Verification Transformation Passes
  • Pipeline guidance