ARIA (Automated Reasoning Infrastructure & Applications) is a toolkit for automated reasoning, which provides a set of tools for constraint solving, theorem proving, and symbolic computation.

Run the following command to setup the local development environment.

bash setup_local_env.sh

The script will

• Create a Python virtual environment if it doesn't exist
• Activate the virtual environment and install dependencies from requirements.txt
• Download required solver binaries (CVC5, MathSAT, z3)
• Run unit tests if available

TBD:

• Test the scripts on different platforms, editors/IDEs, etc.

Local installziation via setup.py

pip install -e .

Then you can use a few cli tools of this library, add call the Python API in your own Python code.

TBD (The repository is not yet released to PyPI.)

Contributions are welcome. Please refer to the repository for detailed instructions on how to contribute.

aria/
├── aria/           # Main library code
├── benchmarks/      # Benchmark files and test cases
├── bin_solvers/     # Binary solver executables
├── docs/            # Documentation files
├── scripts/         # Utility scripts
├── examples/        # A few applications
├── setup.py         # Package setup configuration (not ready)
├── pytest.ini       # PyTest configuration
└── requirements.txt # Project dependencies

For Summer Research, Final Year Project Topics, please refer to docs/topics.rst or TODO.md.

We release the docs here: https://zju-pl.github.io/aria

Another doc generated by deepwiki: https://deepwiki.com/ZJU-PL/aria/1-overview

Here are some of publications related to ARIA.

• ICSE 2024: Enabling Runtime Verification of Causal Discovery Algorithms with Automated Conditional Independence Reasoning. Pingchuan Ma, Zhenlan Ji, Peisen Yao, Shuai Wang, and Kui Ren.
• ICSE 2023: Verifying Data Constraint Equivalence in FinTech Systems. Chengpeng Wang, Gang Fan, Peisen Yao, Fuxiong Pan, and Charles Zhang.
• OOPSLA 2021: Program Analysis via Efficient Symbolic Abstraction. Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang.

• [z3-owl] ranked 3rd in the single-query tracks of QF_ABV, QF_AUFBV, and QF_BVFP at SMT-COMP 2025.

• pysat
• pysmt
• pyqbf
• sympy
• holpy
• iscalc
• amaya
• mypyvy

Primary contributors to this project:

• rainoftime / cutelimination
• JasonJ2021
• ZelinMa557
• Harrywwq
• little-d1d1
• ljcppp
• GooduckZ
• Zahrinas