Lotus is a program analysis, verification, and optimization framework. It provides several toolkits that can be used individually or in combination to perform different tasks. The current version has been tested on x86/ARM Linux and ARM Mac using LLVM-14 with Z3-4.11.

https://zju-pl.github.io/lotus

If you use Lotus in your research or work, please cite the following:

@misc{lotus2025,
  title = {Lotus: A Versatile and Industrial-Scale Program Analysis Framework},
  author = {ZJU Programming Languages and Automated Reasoning Group},
  year = {2025},
  url = {https://github.com/ZJU-PL/lotus},
  note = {Program analysis framework built on LLVM}
}

Papers that use Lotus:

• ISSTA 2025: Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions. Guangsheng Fan, Liqian Chen, Banghu Yin, Wenyu Zhang, Peisen Yao, and Ji Wang.
• S&P 2024: Titan: Efficient Multi-target Directed Greybox Fuzzing. Heqing Huang, Peisen Yao, Hung-Chun Chiu, Yiyuan Guo, and Charles Zhang.
• USENIX Security 2024: Unleashing the Power of Type-Based Call Graph Construction by Using Regional Pointer Information. Yuandao Cai, Yibo Jin, and Charles Zhang.
• TSE 2024: Fast and Precise Static Null Exception Analysis with Synergistic Preprocessing. Yi Sun, Chengpeng Wang, Gang Fan, Qingkai Shi, and Xiangyu Zhang.
• OOPSLA 2022: Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program Analysis. Qingkai Shi, Yongchao Wang, Peisen Yao, and Charles Zhang.

For a detailed list of subsystems (alias analyses, intermediate representations, solvers, abstract interpreters, and utilities), see the Major Components Overview section of the documentation. The docs provide links to the relevant libraries, command-line tools, and example usage for each component.

For detailed documentation on using the binary tools, see tools.

• LLVM 14.x
• Z3 4.11
• CMake 3.10+
• C++14 compatible compiler

git clone https://github.com/ZJU-PL/lotus
cd lotus
mkdir build && cd build
cmake ..
make -j$(nproc)

Notes:

• The build system assumes that the system has a supported LLVM (14.x) and Z3 installed.

• If CMake cannot find LLVM automatically (for example, when using a custom or locally built LLVM), re-run CMake with:

  cmake .. -DLLVM_BUILD_PATH=/path/to/llvm/lib/cmake/llvm

The build system will automatically download and build Boost if it's not found on your system. You can specify a custom Boost installation path with -DCUSTOM_BOOST_ROOT=/path/to/boost.

TODO: Implement automatic download of LLVM and Z3 dependencies

Primary contributors to this project:

• rainoftime / cutelimination
• qingkaishi
• rhuab
• Zahrinas
• Rexxar-Jack-Remar