Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
eldarica [2013/07/09 15:39] hossein |
eldarica [2014/09/23 17:16] hossein [Download] |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== ELDARICA ====== | ====== ELDARICA ====== | ||
+ | |||
+ | ---- | ||
+ | |||
+ | NEW: GitHub link: https://github.com/uuverifiers/eldarica | ||
+ | |||
+ | ---- | ||
| [[http://www.public.asu.edu/~camartin/plants/Plant%20html%20files/pinuseldarica.html|{{ eldarica.jpg?150| }}]] | {{reachability.png?100}} | | | [[http://www.public.asu.edu/~camartin/plants/Plant%20html%20files/pinuseldarica.html|{{ eldarica.jpg?150| }}]] | {{reachability.png?100}} | | ||
Line 14: | Line 20: | ||
For the Z3 connection, Eldarica uses [[https://github.com/psuter/ScalaZ3/|ScalaZ3]]. | For the Z3 connection, Eldarica uses [[https://github.com/psuter/ScalaZ3/|ScalaZ3]]. | ||
- | + | Eldarica can take as input a subset of Scala, or logical representations such as [[http://nts.imag.fr/|Numerical Transition Systems]] and [[https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/|Horn clauses]]. | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
==== Download ==== | ==== Download ==== | ||
Line 33: | Line 29: | ||
* (March 2013): ({{eldarica-1930.jar.gz|JAR file}}) (sp-1930) | * (March 2013): ({{eldarica-1930.jar.gz|JAR file}}) (sp-1930) | ||
* (July 2013): ({{eldarica-2063.jar.gz|JAR file}}) (sp-2063) | * (July 2013): ({{eldarica-2063.jar.gz|JAR file}}) (sp-2063) | ||
+ | * (February 2014): ({{eldarica-2305.jar.gz|JAR file}}) (sp-2305) | ||
+ | We have released the Eldarica source code under the BSD 3-Clause license on [[https://github.com/uuverifiers/eldarica/|Github]]. | ||
+ | We won't post the new releases in this webpage anymore. | ||
==== Related Links ==== | ==== Related Links ==== | ||
Line 42: | Line 40: | ||
* Some {{horn-benchmarks.tar.gz|Horn}} clauses. | * Some {{horn-benchmarks.tar.gz|Horn}} clauses. | ||
* [[horn-nonrec-benchmarks|Non-recursive Horn benchmarks.]] | * [[horn-nonrec-benchmarks|Non-recursive Horn benchmarks.]] | ||
+ | * [[horn-parametric-benchmarks|Parametric Time Automata Horn benchmarks.]] | ||
* [[https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/LIA/Eldarica/|Horn clauses]] in SMT-LIB format. | * [[https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/LIA/Eldarica/|Horn clauses]] in SMT-LIB format. | ||
- | |||
==== Running ==== | ==== Running ==== | ||
\\ | \\ | ||
Line 55: | Line 53: | ||
\\ | \\ | ||
**Eldarica** is being developed and maintained at LARA by [[http://icwww.epfl.ch/~hojjat/| | **Eldarica** is being developed and maintained at LARA by [[http://icwww.epfl.ch/~hojjat/| | ||
- | Hossein Hojjat]] with contributions from [[http://www.philipp.ruemmer.org/|Philipp Ruemmer]]. | + | Hossein Hojjat]] with contributions from [[http://www.philipp.ruemmer.org/|Philipp Ruemmer]] and Filip Konecny. |