Command-Line Tools

Lotus provides various command-line tools for alias analysis, CFL reachability, bug detection, PDG querying, abstract interpretation, and model checking.

This section focuses on the primary front-end binaries built from tools/. The documentation is organized by subdirectory to match the source structure.

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 (sparrow-aa)
  • TPA (tpa)
  • AserPTA (aser-aa)
  • DFPA (dfpa)
  • Call Graph Construction (call-graph)
  • DyckAA (dyck-aa)
  • LotusAA (lotus-aa)
  • FPA (Function Pointer Analysis)
  • Sea-DSA Tools
  • DynAA (Dynamic Alias Analysis)
• CFL Tools
  • Overview
  • CSR: Context-Sensitive Reachability
• Checker Tools
  • lotus-kint – Integer and Array Bug Finder
  • lotus-ae – Abstract Execution Bug Checker
  • lotus-taint – Taint Analysis
  • lotus-concur – Concurrency Bug Checker
  • lotus-saber – Source-Sink Resource Checker
• 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
• 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