Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas

NIAID Data Ecosystem2026-03-12 收录

下载链接：

https://zenodo.org/record/5443614

下载链接

链接失效反馈

官方服务：

资源简介：

## Installation: ``` virtualenv --python=/usr/bin/python3 virenv source virenv/bin/activate cd octopus python3 setup.py install ``` ## Usage: ``` octopus --benchmark=[PATH TO SEED DIRECTORY] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=[SOLVER THEORY] ``` For example: ``` octopus --benchmark=/home/SMT2021 --solverbin=../z3/build/z3 --solver=z3 --theory=LIA ``` To run `n` parallel instances of octopus on `n` cores, use the `--cores` flag. For example: ``` octopus --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA --cores=10 ``` ## Refutational soundness bugs detected so far: octopus has detected many new "refutational soundness" bugs in Z3. Here is a list of issues we reported. https://github.com/Z3Prover/z3/issues/5373 `[z3]` `[QF_NRA]` https://github.com/Z3Prover/z3/issues/5443 `[z3]` `[QF_BVFP]` https://github.com/Z3Prover/z3/issues/5447 `[z3]` `[QF_ABV]` https://github.com/Z3Prover/z3/issues/5456 `[z3]` `[QF_IDL]` https://github.com/Z3Prover/z3/issues/5457 `[z3]` `[QF_BV]` https://github.com/Z3Prover/z3/issues/5460 `[z3]` `[QF_BV]` https://github.com/Z3Prover/z3/issues/5468 `[z3]` `[AUFLIRA]` https://github.com/Z3Prover/z3/issues/5488 `[z3]` `[QF_BV]` https://github.com/Z3Prover/z3/issues/5502 `[z3]` `[QF_NIA]` https://github.com/Z3Prover/z3/issues/5508 `[z3]` `[QF_NIA]` https://github.com/Z3Prover/z3/issues/5423 `[z3]` `[QF_BVFP]` `Won't fixed`

创建时间：

2021-09-06

5,000+

优质数据集

54 个

任务类型

进入经典数据集