This project is funded (subject to contract) as project H2020-FETOPN-2015-CSA_712689 of the European Union. It is the start of the general push to create a real SC2 community. More details can be found on the SC2 announcement poster, which is popular on ResearchGate.


The use of advanced methods to solve practical and industrially relevant problems by computers has a long history. Whereas Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems, more recent developments in the area of Satisfiability Checking tackle similar problems but with different algorithmic and technological solutions. Though both communities have made remarkable progress in the last decades, they still need to be strengthened to tackle practical problems of rapidly increasing size and complexity. Their separate tools (computer algebra systems and SMT solvers) are urgently needed to examine prevailing problems with a direct effect to our society. For example, Satisfiability Checking is an essential backend for assuring the security and the safety of computer systems. In various scientific areas, Symbolic Computation enables dealing with large mathematical problems out of reach of pencil and paper developments. Currently the two communities are largely disjoint and unaware of the achievements of each other, despite strong reasons for them to discuss and collaborate, as they share many central interests. However, researchers from these two communities rarely interact, and also their tools lack common, mutual interfaces for unifiying their strengths. Bridges between the communities in the form of common platforms and roadmaps are necessary to initiate an exchange, and to support and to direct their interaction. These are the main objectives of this CSA. We will initiate a wide range of activities to bring the two communities together, identify common challenges, offer global events and bilateral visits, propose standards, and so on. We believe that these activities will initiate cross-fertilisation of both fields and bring mutual improvements. Combining the knowledge, experience and the technologies in these communities will enable the development of radically improved software tools


The SC2 summer school will take place in Saarbr├╝cken from Monday, July 31st, to Friday, August 4th, 2017.

SC-square will have its second formal workshop in Kaiserslautern Saturday 29th July (and if necessary Sunday 30th), immediately after ISSAC 2017 and before the SC2 summer school in nearby Saarbr├╝cken.

In January 2017 the EU approved an expanded list of external experts, all of whom become associates of SC-square.

SC-square had its first formal workshop at SYNASC 2016. There were also an SCSC thematic session just before, at CASC 2016.

A SC2 thematic session took place on Tuesday September 20th at CASC 2016 (Bucharest).

Click here to download the SC-square Announcement Poster.

On February 28th, 2016, the European Commission announced an intention to fund this project, which started on 1 July 2016, running to 31 August 2018.

SC2 Project Documents

Various templates for reporting are at this location.

SC2 Activities

DatesEventSC2 activity
1-4 August 2016 ACA 2016 (Kassel) SC2 session
Also automatic proving and dynamic geometry (see also here)
19-23 September 2016CASC 2016 (Bucharest)SC2 thematic session
24-27 September 2016SYNASC 2016 (Timisoara)First SCSC-CSA workshop
Note that this is adjacent in time, and in the same country as, CASC
(Also Laura Kovacs)
29 JulyISSAC 2017 (Kaiserslautern)The 2nd SC2 Workshop
31 July - 04 August 2017The SC2 summer school

Related Activities

DatesEventRelated activity
27-29 June 2016ADG 2016 (Strasbourg)(N.B. out of grant period, financially)
11-14 July 2016ICMS 2016 (Berlin)Several submissions, SC2 poster
25-29 July 2016CICM 2016 (Bialystok)Various talks/sessions
22-27 August 2016 ITP 2016: Interactive Theorem Proving (Nancy)Grant Passmore, at least


The overall aim of this project is to create a new research community bridging the gap between Satisfiability Checking and Symbolic Computation, whose members will ultimately be well informed about both fields, and thus able to combine the knowledge and techniques of both fields to develop new research and to resolve problems (both academic and industrial) currently beyond the scope of either individual field.


University of Bath James Davenport; Russell Bradford
RWTH Aachen Erika Ábrahám; Viktor Levandovskyy
Fondazione Bruno Kessler Alberto Griggio; Alessandro Cimatti
Università degli Studi di Genova Anna Bigatti
Maplesoft Europe Ltd Jürgen Gerhard; Stephen Forrest
Université de Lorraine (LORIA) Pascal Fontaine
Coventry University Matthew England
University of Oxford Daniel Kroening; Martin Brain
Universität Kassel Werner Seiler; John Abbott
Max Planck Institut für Informatik Thomas Sturm
Universität Linz Tudur Jebelean; Bruno Buchberger; Wolfgang Windsteiger; Roxana-Maria Holom