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:

1. fork from Paradoxika/Skeptik,
2. program according to the usual Scala style conventions,
3. follow the git flow branching model in their own forks,
4. 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

• Bruno Woltzenlogel Paleo
• Joseph Boudou
• Andreas Fellner
• Jan Gorzny

Full list of contributors

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. thesis or Ph.D. thesis related to Skeptik, please contact Bruno Woltzenlogel Paleo

Communication Channels

• Skeptik's Mailinglist for Developers

Support

• Skeptik was supported by Google Summer of Code 2017
• Skeptik was supported by Google Summer of Code 2016
• Skeptik was supported by Google Summer of Code 2015
• 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

Licenses

• GNU-GPL-3.0

• CC-By-NC-SA