Skeptik is a collection of data structures and algorithms focused especially on the compression of formal proofs.
Resolution proofs, in particular, are used by various sat-solvers, smt-solvers and automated theorem provers, as certificates of correctness for the answers they provide. These automated deduction tools have a wide range of application areas, from mathematics to software and hardware verification.
By providing smaller resolution proofs that are easier and faster to check, Skeptik aims at improving the reliability of these automated deduction tools and at facilitating the exchange of information between them.
###Usage Instructions###
Tell your java virtual machine to use UTF-8 and more memory. You can do this by setting your environment variable with the following command:
$ export JAVA_TOOL_OPTIONS="-Dfile.encoding=UTF-8 -Xmx1024m -Xss4m -XX:MaxPermSize=256m"
(you may change the values after -Xmx
, Xss
and XX:MaxPermSize=
to suit your needs)
You must have SBT (version >= 0.13) installed. SBT automatically downloads all compilers and libraries on which Skeptik depends.
To start SBT, go to Skeptik's home folder using the terminal and run:
$ sbt
You can run skeptik within SBT's command line. With the following SBT command, skeptik will be compiled and executed, and a help message will be shown.
> skeptik --help
The following command processes the proof 'eq_diamond9.smt2' using the algorithms 'RP' and the sequential composition of 'D', 'RPI' and 'LU'. The compressed proofs are written using the 'smt2' proof format.
> skeptik -a RP -a (D-RPI-LU) -f smt2 examples/proofs/VeriT/eq_diamond9.smt2
To use skeptik from outside SBT, a jar file must be generated by executing the following command within SBT:
> one-jar
The generated jar file can be deployed and used like any other java jar file:
$ java -jar skeptik.jar -a RP -a (D-RPI-LU) -f smt2 examples/proofs/VeriT/eq_diamond9.smt2
###Skeptik as a Library###
To import Skeptik as a library in your own Java or Scala projects,
add the following line to your build.sbt file, if you are using SBT to manage the library dependencies of your project:
libraryDependencies += "at.logic" %% "skeptik" % "1.0"
or add the following lines to your pom.xml file, if you are using Maven instead:
<dependency>
<groupId>at.logic</groupId>
<artifactId>skeptik_2.10</artifactId>
<version>1.0</version>
</dependency>
###Stats###
###Development Policy###
Developers are encouraged to:
- fork from Paradoxika/Skeptik,
- program according to the usual Scala style conventions,
- follow the git flow branching model in their own forks,
- make pull requests when they have finished a feature or hotfix branch.
Using the git flow model can be easier with the gitflow extension for git.
###Documentation###
Detailed theoretical descriptions of some of the algorithms implemented in Skeptik are available in our papers. There are also slides of presentations about Skeptik.
Scaladoc documentation for the code can be generated by running the following command:
sbt doc
###Active Developers###
###Job Opportunities###
- Google Summer of Code grants are available every year. If you would like to apply, it is never too early to contact us.
- If you would like to do a project, M.Sc. or Ph.D. at TU-Wien related to Skeptik, please contact Bruno Woltzenlogel Paleo
###Communication Channels###
- Skeptik's Mailinglist for Developers
- IRC Channel on freenode: #Skeptik
###Support###
- Skeptik's development is currently funded by the Austrian Science Fund (Project P24300)
- Skeptik was supported by Google Summer of Code 2013
- Skeptik was supported by Google Summer of Code 2012
- A free license of YourKit profiler helps us keep Skeptik's code fast and leak-free
- Fast experiments on thousands of large proofs are made possible by the Vienna Scientific Cluster