storm

storm copied to clipboard

Installation:

git clone https://github.com/Practical-Formal-Methods/storm
virtualenv --python=/usr/bin/python3.7 venv
source venv/bin/activate
cd storm
python setup.py install

Usage:

storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME]

To test the solver on a particular theory, use the --theory flag. For example:

storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA

To run n parallel instances of storm on n cores, use the --cores flag. For example:

storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA --cores=10

To obtain a smaller SMT instance that revealed a refutational soundness bug in an SMT solver, use:

storm --min --file_path=[PATH TO SMT INSTANCE] --solver=[SOLVER NAME] --solverbin=[PATH TO SOLVER BIN] --theory=[THEORY NAME] 

If the SMT instance is in incremental mode, use --incremental flag.

Soundness bugs detected so far:

STORM has detected many unique and previously unknown "refutational soundness" bugs in multiple mature SMT solvers. Here is a list of issues we filed on public bug tracking systems for various SMT solvers.

https://github.com/SRI-CSL/yices2/issues/150 [yices] [QF_UFIDL]
https://github.com/SRI-CSL/yices2/issues/160 [yices] [QF_UFLRA]
https://github.com/SRI-CSL/yices2/issues/167 [yices] [QF_UF]
https://github.com/Z3Prover/z3/issues/2758 [z3] [QF_S]
https://github.com/Z3Prover/z3/issues/3067 [z3str3] [QF_S]
https://github.com/levnach/z3/issues/115 [z3] [QF_NIA]
https://github.com/levnach/z3/issues/116 [z3] [QF_NRA]
https://github.com/Z3Prover/z3/issues/2828 [z3] [QF_S]
https://github.com/Z3Prover/z3/issues/2871 [z3] [QF_LIA]
https://github.com/SRI-CSL/yices2/issues/170 [yices] [QF_NRA]
https://github.com/Z3Prover/z3/issues/2829 [z3] [QF_LIA]
https://github.com/Z3Prover/z3/issues/2835 [z3] [QF_UFLIA]
https://github.com/Z3Prover/z3/issues/2873 [z3] [QF_BV]
https://github.com/Z3Prover/z3/issues/2993 [z3] [QF_S]
https://github.com/levnach/z3/issues/114 [z3] [AUFNIRA]
https://github.com/Z3Prover/z3/issues/3052 [z3] [LIA]
https://github.com/Z3Prover/z3/issues/3058 [z3] [QF_BVFP]
https://github.com/Z3Prover/z3/issues/3068 [z3] [UF]
https://github.com/SRI-CSL/yices2/issues/169 [yices] [QF_UFIDL]
https://github.com/SRI-CSL/yices2/issues/170 [yices] [QF_NRA]
https://github.com/Z3Prover/z3/issues/2994 [z3str3] [QF_S]
https://github.com/Z3Prover/z3/issues/3031 [z3str3] [QF_S]
https://github.com/Z3Prover/z3/issues/2916 [z3] [QF_S]
https://github.com/Z3Prover/z3/issues/2925 [z3] [QF_FP]
https://github.com/Z3Prover/z3/issues/3040 [z3] [QF_BV]
https://github.com/Z3Prover/z3/issues/3096 [z3] [QF_NIA]
https://github.com/Z3Prover/z3/issues/3256 [z3] [AUFNIRA]
https://github.com/Z3Prover/z3/issues/3822 [z3] [BV]
https://github.com/Z3Prover/z3/issues/3948 [z3] [AUFDTLIA]
https://github.com/Z3Prover/z3/issues/3949 [z3] [QF_UFLRA]
https://github.com/Z3Prover/z3/issues/4590 [z3str3] [QF_S]
https://github.com/SRI-CSL/yices2/issues/280 [yices] [QF_NRA]

Reproducing bugs used in the evaluation section of our ESEC/FSE 2020 paper:

Please follow the instructions here.