Initial commit

.github/workflows/python-app.yml

@@ -0,0 +1,36 @@
+# This workflow will install Python dependencies, run tests and lint with a single version of Python
+# For more information see: https://help.github.com/actions/language-and-framework-guides/using-python-with-github-actions
+
+name: Python application
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up Python 3.8
+      uses: actions/setup-python@v2
+      with:
+        python-version: 3.8
+    - name: Install dependencies
+      run: |
+        python -m pip install --upgrade pip
+        pip install flake8 pytest
+        if [ -f requirements.txt ]; then pip install -r requirements.txt; fi
+    - name: Lint with flake8
+      run: |
+        # stop the build if there are Python syntax errors or undefined names
+        flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics
+        # exit-zero treats all errors as warnings. The GitHub editor is 127 chars wide
+        flake8 . --count --exit-zero --max-complexity=10 --max-line-length=127 --statistics
+    - name: Test with pytest
+      run: |
+        pytest

.github/workflows/python-package.yml

@@ -0,0 +1,39 @@
+# This workflow will install Python dependencies, run tests and lint with a variety of Python versions
+# For more information see: https://help.github.com/actions/language-and-framework-guides/using-python-with-github-actions
+
+name: Python package
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        python-version: [3.5, 3.6, 3.7, 3.8]
+
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up Python ${{ matrix.python-version }}
+      uses: actions/setup-python@v2
+      with:
+        python-version: ${{ matrix.python-version }}
+    - name: Install dependencies
+      run: |
+        python -m pip install --upgrade pip
+        pip install flake8 pytest
+        if [ -f requirements.txt ]; then pip install -r requirements.txt; fi
+    - name: Lint with flake8
+      run: |
+        # stop the build if there are Python syntax errors or undefined names
+        flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics
+        # exit-zero treats all errors as warnings. The GitHub editor is 127 chars wide
+        flake8 . --count --exit-zero --max-complexity=10 --max-line-length=127 --statistics
+    - name: Test with pytest
+      run: |
+        pytest

.gitignore

@@ -0,0 +1,28 @@
+.idea/*
+build/*
+dist/*
+storm.egg-info/*
+temp/*
+.DS_Store
+config.py
+storm/fse_repl/bug1/mutant_*
+storm/fse_repl/bug2/mutant_*
+storm/fse_repl/bug3/mutant_*
+storm/fse_repl/bug4/mutant_*
+storm/fse_repl/bug5/mutant_*
+storm/fse_repl/bug6/mutant_*
+storm/fse_repl/bug7/mutant_*
+storm/fse_repl/bug8/mutant_*
+storm/fse_repl/bug9/mutant_*
+storm/fse_repl/bug10/mutant_*
+storm/fse_repl/bug11/mutant_*
+storm/fse_repl/bug12/mutant_*
+storm/fse_repl/bug13/mutant_*
+storm/fse_repl/bug14/mutant_*
+storm/fse_repl/bug15/mutant_*
+storm/fse_repl/bug16/mutant_*
+storm/fse_repl/bug17/mutant_*
+storm/fse_repl/bug18/mutant_*
+storm/fse_repl/bug19/mutant_*
+storm/fse_repl/bug20/mutant_*
+storm/fse_repl/bug21/mutant_*

README.md

@@ -0,0 +1,80 @@
+![logo](https://user-images.githubusercontent.com/4897599/72667625-29075e00-3a1e-11ea-8179-776e9c4c938d.png)
+
+![Python application](https://github.com/Practical-Formal-Methods/storm/workflows/Python%20application/badge.svg)
+![Python package](https://github.com/Practical-Formal-Methods/storm/workflows/Python%20package/badge.svg)
+
+## 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]` <br>
+https://github.com/SRI-CSL/yices2/issues/160 `[yices]` `[QF_UFLRA]` <br>
+https://github.com/SRI-CSL/yices2/issues/167 `[yices]` `[QF_UF]` <br>
+https://github.com/Z3Prover/z3/issues/2758 `[z3]` `[QF_S]` <br>
+https://github.com/Z3Prover/z3/issues/3067 `[z3str3]` `[QF_S]` <br>
+https://github.com/levnach/z3/issues/115 `[z3]` `[QF_NIA]` <br>
+https://github.com/levnach/z3/issues/116 `[z3]` `[QF_NRA]` <br>
+https://github.com/Z3Prover/z3/issues/2828 `[z3]` `[QF_S]` <br>
+https://github.com/Z3Prover/z3/issues/2871 `[z3]` `[QF_LIA]` <br>
+https://github.com/SRI-CSL/yices2/issues/170 `[yices]` `[QF_NRA]` <br>
+https://github.com/Z3Prover/z3/issues/2829 `[z3]` `[QF_LIA]` <br>
+https://github.com/Z3Prover/z3/issues/2835 `[z3]` `[QF_UFLIA]` <br>
+https://github.com/Z3Prover/z3/issues/2873 `[z3]` `[QF_BV]` <br>
+https://github.com/Z3Prover/z3/issues/2993 `[z3]` `[QF_S]` <br>
+https://github.com/levnach/z3/issues/114 `[z3]` `[AUFNIRA]` <br>
+https://github.com/Z3Prover/z3/issues/3052 `[z3]` `[LIA]` <br>
+https://github.com/Z3Prover/z3/issues/3058 `[z3]` `[QF_BVFP]` <br>
+https://github.com/Z3Prover/z3/issues/3068 `[z3]` `[UF]` <br>
+https://github.com/SRI-CSL/yices2/issues/169 `[yices]` `[QF_UFIDL]` <br>
+https://github.com/SRI-CSL/yices2/issues/170 `[yices]` `[QF_NRA]` <br>
+https://github.com/Z3Prover/z3/issues/2994 `[z3str3]` `[QF_S]` <br>
+https://github.com/Z3Prover/z3/issues/3031 `[z3str3]` `[QF_S]` <br>
+https://github.com/Z3Prover/z3/issues/2916 `[z3]` `[QF_S]` <br>
+https://github.com/Z3Prover/z3/issues/2925 `[z3]` `[QF_FP]` <br>
+https://github.com/Z3Prover/z3/issues/3040 `[z3]` `[QF_BV]` <br>
+https://github.com/Z3Prover/z3/issues/3096 `[z3]` `[QF_NIA]` <br>
+https://github.com/Z3Prover/z3/issues/3256 `[z3]` `[AUFNIRA]` <br>
+https://github.com/Z3Prover/z3/issues/3822 `[z3]` `[BV]` <br>
+https://github.com/Z3Prover/z3/issues/3948 `[z3]` `[AUFDTLIA]` <br>
+https://github.com/Z3Prover/z3/issues/3949 `[z3]` `[QF_UFLRA]` <br>
+https://github.com/Z3Prover/z3/issues/4590 `[z3str3]` `[QF_S]` <br>
+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](https://github.com/Practical-Formal-Methods/storm/tree/master/storm/fse_repl).

docs/Gemfile

@@ -0,0 +1,5 @@
+# frozen_string_literal: true
+
+source 'https://rubygems.org'
+
+gemspec

docs/LICENSE

@@ -0,0 +1,116 @@
+CC0 1.0 Universal
+
+Statement of Purpose
+
+The laws of most jurisdictions throughout the world automatically confer
+exclusive Copyright and Related Rights (defined below) upon the creator and
+subsequent owner(s) (each and all, an "owner") of an original work of
+authorship and/or a database (each, a "Work").
+
+Certain owners wish to permanently relinquish those rights to a Work for the
+purpose of contributing to a commons of creative, cultural and scientific
+works ("Commons") that the public can reliably and without fear of later
+claims of infringement build upon, modify, incorporate in other works, reuse
+and redistribute as freely as possible in any form whatsoever and for any
+purposes, including without limitation commercial purposes. These owners may
+contribute to the Commons to promote the ideal of a free culture and the
+further production of creative, cultural and scientific works, or to gain
+reputation or greater distribution for their Work in part through the use and
+efforts of others.
+
+For these and/or other purposes and motivations, and without any expectation
+of additional consideration or compensation, the person associating CC0 with a
+Work (the "Affirmer"), to the extent that he or she is an owner of Copyright
+and Related Rights in the Work, voluntarily elects to apply CC0 to the Work
+and publicly distribute the Work under its terms, with knowledge of his or her
+Copyright and Related Rights in the Work and the meaning and intended legal
+effect of CC0 on those rights.
+
+1. Copyright and Related Rights. A Work made available under CC0 may be
+protected by copyright and related or neighboring rights ("Copyright and
+Related Rights"). Copyright and Related Rights include, but are not limited
+to, the following:
+
+  i. the right to reproduce, adapt, distribute, perform, display, communicate,
+  and translate a Work;
+
+  ii. moral rights retained by the original author(s) and/or performer(s);
+
+  iii. publicity and privacy rights pertaining to a person's image or likeness
+  depicted in a Work;
+
+  iv. rights protecting against unfair competition in regards to a Work,
+  subject to the limitations in paragraph 4(a), below;
+
+  v. rights protecting the extraction, dissemination, use and reuse of data in
+  a Work;
+
+  vi. database rights (such as those arising under Directive 96/9/EC of the
+  European Parliament and of the Council of 11 March 1996 on the legal
+  protection of databases, and under any national implementation thereof,
+  including any amended or successor version of such directive); and
+
+  vii. other similar, equivalent or corresponding rights throughout the world
+  based on applicable law or treaty, and any national implementations thereof.
+
+2. Waiver. To the greatest extent permitted by, but not in contravention of,
+applicable law, Affirmer hereby overtly, fully, permanently, irrevocably and
+unconditionally waives, abandons, and surrenders all of Affirmer's Copyright
+and Related Rights and associated claims and causes of action, whether now
+known or unknown (including existing as well as future claims and causes of
+action), in the Work (i) in all territories worldwide, (ii) for the maximum
+duration provided by applicable law or treaty (including future time
+extensions), (iii) in any current or future medium and for any number of
+copies, and (iv) for any purpose whatsoever, including without limitation
+commercial, advertising or promotional purposes (the "Waiver"). Affirmer makes
+the Waiver for the benefit of each member of the public at large and to the
+detriment of Affirmer's heirs and successors, fully intending that such Waiver
+shall not be subject to revocation, rescission, cancellation, termination, or
+any other legal or equitable action to disrupt the quiet enjoyment of the Work
+by the public as contemplated by Affirmer's express Statement of Purpose.
+
+3. Public License Fallback. Should any part of the Waiver for any reason be
+judged legally invalid or ineffective under applicable law, then the Waiver
+shall be preserved to the maximum extent permitted taking into account
+Affirmer's express Statement of Purpose. In addition, to the extent the Waiver
+is so judged Affirmer hereby grants to each affected person a royalty-free,
+non transferable, non sublicensable, non exclusive, irrevocable and
+unconditional license to exercise Affirmer's Copyright and Related Rights in
+the Work (i) in all territories worldwide, (ii) for the maximum duration
+provided by applicable law or treaty (including future time extensions), (iii)
+in any current or future medium and for any number of copies, and (iv) for any
+purpose whatsoever, including without limitation commercial, advertising or
+promotional purposes (the "License"). The License shall be deemed effective as
+of the date CC0 was applied by Affirmer to the Work. Should any part of the
+License for any reason be judged legally invalid or ineffective under
+applicable law, such partial invalidity or ineffectiveness shall not
+invalidate the remainder of the License, and in such case Affirmer hereby
+affirms that he or she will not (i) exercise any of his or her remaining
+Copyright and Related Rights in the Work or (ii) assert any associated claims
+and causes of action with respect to the Work, in either case contrary to
+Affirmer's express Statement of Purpose.
+
+4. Limitations and Disclaimers.
+
+  a. No trademark or patent rights held by Affirmer are waived, abandoned,
+  surrendered, licensed or otherwise affected by this document.
+
+  b. Affirmer offers the Work as-is and makes no representations or warranties
+  of any kind concerning the Work, express, implied, statutory or otherwise,
+  including without limitation warranties of title, merchantability, fitness
+  for a particular purpose, non infringement, or the absence of latent or
+  other defects, accuracy, or the present or absence of errors, whether or not
+  discoverable, all to the greatest extent permissible under applicable law.
+
+  c. Affirmer disclaims responsibility for clearing rights of other persons
+  that may apply to the Work or any use thereof, including without limitation
+  any person's Copyright and Related Rights in the Work. Further, Affirmer
+  disclaims responsibility for obtaining any necessary consents, permissions
+  or other rights required for any use of the Work.
+
+  d. Affirmer understands and acknowledges that Creative Commons is not a
+  party to this document and has no duty or obligation with respect to this
+  CC0 or use of the Work.
+
+For more information, please see
+<http://creativecommons.org/publicdomain/zero/1.0/>