Google Summer of Code

  • The computer science and engineering group of the Vienna University of Technology has been accepted as a mentoring organization for the 3rd consecutive year in Google's Summer of Code program (…oogle/gsoc2013/cse_tuwien), and *Skeptik* ( is one of its projects.

    Skeptik is a tool for checking, compressing and improving formal proofs generated by automated deduction tools, currently focusing on propositional resolution proofs generated by Sat- and SMT-solvers. It implements various recent proof compression algorithms, such as RecyclePivots, RecyclePivotsWithIntersection, Split, Reduce&Reconstruct, LowerUnits, LowerUnivalents, as well as combinations and variants of these algorithms.

    Students interested in applying for a Google Summer of Code grant (US$ 5000) to work from 17th of June to 23rd of September on the development of new proof compression algorithms within Skeptik should follow the instructions in this wiki-page:

    The *DEADLINE* for student applications is 3rd of May 2013.

    Before preparing their applications, students are encouraged to contact us (preferably by sending a message to our mailinglist (…mailman/listinfo/soc2013/) with "[Skeptik]" in the subject).

    Best regards,

    Bruno Woltzenlogel Paleo
    Theory and Logic Group
    Vienna University of Technology