Command-Line Tools

Lotus provides command-line tools for alias analysis, CFL reachability, bug detection, IR querying, optimization, verification, and solver experiments.

This section focuses on the front-end binaries and tool families under tools/. The documentation is organized by subdirectory to match the source structure, but some pages also note when a tool family contains source-present experiments that are not built by default.

For a feature-oriented walk-through, see Tutorials and Examples and Bug Detection with Lotus.

Tools by Subdirectory

The documentation is organized to match the tools/ directory structure:

• Alias Analysis Tools
  • SparrowAA (lotus-alias-sparrow-aa)
  • TPA (lotus-alias-tpa)
  • AserPTA (lotus-alias-aser-aa)
  • DFPA (dfpa)
  • Call Graph Construction (lotus-alias-call-graph)
  • DyckAA (lotus-alias-dyck-aa)
  • LotusAA (lotus-alias-lotus-aa)
  • FPA (Function Pointer Analysis)
  • Sea-DSA Tools
  • DynAA (Dynamic Alias Analysis)
• CFL Tools
  • Overview
  • CSR: Context-Sensitive Reachability
• Checker Tools
  • Unified Frontend
  • Basic Usage
  • Subcommand Examples
  • See Also
• Dataflow Tools
  • Overview
  • lotus-dfa
  • lotus-dfa-apa
  • lotus-dfa-mono
  • lotus-dfa-ifds
  • See also
• PDG Query – Program Dependence Graph Queries
  • PDG Query Example Cookbook
• Optimization Tools
  • Inter-Procedural Optimizations
  • Prefetch Optimization Tool
• Solver Tools
  • OWL – SMT/Model Checking Front-End
  • SLOT – SMT-LIB to LLVM Translator
  • STAUB – Bounded-Theory Conversion Front-End
• Verifier Tools
  • CLAM – Numerical Abstract Interpretation
  • SymAbsAI – Symbolic Abstraction + Abstract Interpretation
  • Sifa – Symbolic Interpretation with Fluid Abstractions
  • SeaHorn – Verification Framework
  • Horn-ICE – CHC Verification with Learning