| 1 | SARL: Symbolic Algebra and Reasoning Library
|
|---|
| 2 | http://vsl.cis.udel.edu/sarl
|
|---|
| 3 |
|
|---|
| 4 | =============================== ABOUT =================================
|
|---|
| 5 |
|
|---|
| 6 | SARL is a Java library for symbolic algebra and reasoning.
|
|---|
| 7 | It is intended primarily to support symbolic execution.
|
|---|
| 8 |
|
|---|
| 9 | The SARL API provides for the creation and manipulation of typed
|
|---|
| 10 | symbolic expressions, and the ability to verify the validity of first
|
|---|
| 11 | order formulas.
|
|---|
| 12 |
|
|---|
| 13 | SARL uses ("under the hood") automated theorem provers (currently
|
|---|
| 14 | CVC3 and CVC4) to assist in the verification tasks. It also is
|
|---|
| 15 | very effective at placing symbolic expressions in a canonical form,
|
|---|
| 16 | in order to easily tell if two expressions are equivalent. It
|
|---|
| 17 | supports real (mathematical) integers and reals, as well as
|
|---|
| 18 | Herbrand integers and reals (where the numeric operations are
|
|---|
| 19 | treated as uninterpreted functions).
|
|---|
| 20 |
|
|---|
| 21 | SARL is written by Stephen Siegel, University of Delaware.
|
|---|
| 22 | Please send comments, bug reports, feature requests, etc., to
|
|---|
| 23 | siegel@udel.edu.
|
|---|
| 24 |
|
|---|
| 25 | ============================ INSTALLATION =============================
|
|---|
| 26 |
|
|---|
| 27 | If you only want to use SARL (and not contribute to its development)
|
|---|
| 28 | you only need to download/install the automated theorem provers
|
|---|
| 29 | CVC3 and CVC4 and then download sarl.jar and place it in the CLASSPATH
|
|---|
| 30 | for your application. See file INSTALL in this directory.
|
|---|
| 31 |
|
|---|
| 32 | In order for SARL to find CVC3 and CVC4, the executables (cvc3 and
|
|---|
| 33 | cvc4) must be in your PATH the first time you use SARL.
|
|---|
| 34 |
|
|---|
| 35 | You will also need a Java 8 SDK.
|
|---|
| 36 |
|
|---|
| 37 | If you want to install from source (e.g., because you want to develop
|
|---|
| 38 | SARL), it is a bit more complicated, because SARL requires
|
|---|
| 39 | all of the following:
|
|---|
| 40 |
|
|---|
| 41 | - Java SE 8 SDK
|
|---|
| 42 | http://www.oracle.com/technetwork/java/javase/downloads/index.html
|
|---|
| 43 | - Apache Ant (build tool):
|
|---|
| 44 | http://ant.apache.org
|
|---|
| 45 | - CVC3 (automated theorem prover):
|
|---|
| 46 | http://www.cs.nyu.edu/acsys/cvc3/download.html
|
|---|
| 47 | - CVC4 (automated theorem prover):
|
|---|
| 48 | http://cvc4.cs.nyu.edu/downloads/
|
|---|
| 49 | - Z3 (automated theorem prover)
|
|---|
| 50 | http://z3.codeplex.com/SourceControl/latest
|
|---|
| 51 | - JUnit (automated testing framework):
|
|---|
| 52 | https://github.com/KentBeck/junit/downloads
|
|---|
| 53 | - Hamcrest (a library of "matchers", required by JUnit):
|
|---|
| 54 | https://github.com/hamcrest/JavaHamcrest
|
|---|
| 55 | - JaCoCo (Java code coverage analysis tool):
|
|---|
| 56 | http://www.jacoco.org
|
|---|
| 57 |
|
|---|
| 58 | See file INSTALL in this directory for detailed instructions on
|
|---|
| 59 | installing SARL from source.
|
|---|
| 60 |
|
|---|
| 61 | ============================== LICENSES ===============================
|
|---|
| 62 |
|
|---|
| 63 | SARL is copyright 2013,2014, Stephen F. Siegel,
|
|---|
| 64 | Verified Software Laboratory, University of Delaware.
|
|---|
| 65 | It is distributed under the terms of the GNU
|
|---|
| 66 | Lesser General Public License (LGPL).
|
|---|
| 67 | See the file COPYING.LESSER.
|
|---|
