Lotus

User Guide

  • Major Components Overview
  • Architecture Overview
  • Quick Start Guide
  • Installation Guide
  • Tutorials and Examples
  • Bug Detection with Lotus
  • PDG Query Language (Cypher)
  • Property-Based Slicing
  • Verification Backend Abstraction
  • Instrumentation Passes
  • Troubleshooting and FAQ
  • Command-Line Tools

Core Components

  • Alias Analysis
  • Analysis Framework
  • Annotations
  • Applications
  • Context-Free Language Analysis
  • Data Flow Analysis
  • Intermediate Representations
  • Overview
  • MemoryMLFeaturesPass
  • Features Extracted
  • Feature Output
  • Analysis Dependencies
  • Integration Notes
  • Related Components
  • Optimization
  • Security Components
  • Solvers
  • Transforms
  • Utilities
  • Verification
    • Verification Support Analyses
    • Verification Backend API
    • CRAB - Abstract Interpretation Library
    • CLAM – Abstract Interpretation Framework
    • SMACK Verification Frontend
    • Sifa
    • SymAbsAI – Symbolic Abstraction + Abstract Interpretation
    • SeaHorn Verification Framework
    • Failure-Directed Trimming
    • Verification Transformation Passes
  • Checker Framework

Developer Documentation

  • API Reference
  • Developer Guide
Lotus
  • Verification
  • View page source

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
  • SymAbsAI – Symbolic Abstraction + Abstract Interpretation
  • SeaHorn Verification Framework
    • Overview
    • Structure
    • Components
    • SeaHorn Verification
  • Failure-Directed Trimming
    • Overview
    • Use cases
    • Notes
  • Verification Transformation Passes
Previous Next

© Copyright 2024-2025, ZJU Programming Languages and Automated Reasoning Group.

Built with Sphinx using a theme provided by Read the Docs.