SC2 Summer School 2017

The school introduces graduate students and researchers from academia and industry into research and methodology in both Satisfiability Checking (SAT/SMT) and Symbolic Computation with one focus on their interconnections. It combines a thorough introduction into the theory of both fields with lectures on state-of-the-art software systems and their implementation. This is supplemented with presentations by lecturers from industry discussing the practical relevance of the topics of the school.

Time and place: July 31-August 4, 2017, MPI Informatics, Saarbrücken, Germany

This project has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689.


Please send questions about the summer school to


  • SAT checking
  • SMT solving theory and software
  • computer algebra theory and systems
  • cylindrical algebraic decomposition
  • industrial applications of satisfiability and symbolic computation
  • basics of first-order theorem proving and interactive higher order proving