Summary
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.
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.
Latest SC2 News
Proposed constitution for the 2 Workshop Series available here (2018/07/11).
There will be a Journal of Symbolic Computation Special Issue on SC2.
Click here for full details.
SC2 Events
| Dates | Event | SC2 Activity |
| 1-4 August 2016 | ACA 2016 (Kassel) | SC2 Session |
| Also SC2 contributions to Automatic Proving and Dynamic Geometry Session. | ||
| 19-23 September 2016 | CASC 2016 (Bucharest) | SC2 Thematic Session |
| 24-27 September 2016 | SYNASC 2016 (Timisoara) | The First SC2 Workshop (Proceedings) |
| 29 July 2017 | ISSAC 2017 (Kaiserslautern) | The Second SC2 Workshop (Proceedings) |
| 31 July - 04 August 2017 | The SC2 Summer School (Saarbrucken) | Videos here |
| 11 July 2018 | FLoC 2018 (Oxford) | The Third SC2 Workshop |
| 24-27 July 2018 | ICMS 2018 (Notre Dame, Indiana, USA) | SC2 Session |
Related Activities
| Dates | Event | SC2 Activity |
| 27-29 June 2016 | ADG 2016 (Strasbourg, France) | (N.B. out of grant period, financially) |
| 5-8 July 2016 | LICS 2016 (New York, USA) | Paper, SC2 poster |
| 11-14 July 2016 | ICMS 2016 (Berlin, Germany) | Several papers, SC2 poster |
| 20-22 July 2016 | ISSAC 2016 (Waterloo, Canada) | SC2 Poster |
| 25-29 July 2016 | CICM 2016 (Bialystok, Poland) | Various talks/sessions inc. SC2 Project Paper |
| 30 March - 1 April 2017 | AAA 2017 (Pisa, Italy) | Talks by 3 consortium members and an associate |
| 22-29 April 2017 | TACAS 2017 (Uppsala, Sweden) | Paper |
| 4-6 May 2017 | Fachgruppe Computer Algebra Meeting (Kassel, Germany) | SC2 Poster and discussions |
| 17-21 July 2017 | CICM 2017 (Edinburgh, UK) | SMT-LIB paper in the OpenMath Session |
| 22-23 July 2017 | SMT 2017 (Heidelberg, Germany) | Papers, and JHD gives invited talk on SC2. |
| 6 August 2017 | ARCADE 2017 (Gothenberg, Sweeden) | SC2 Paper |
| 8-11 August 2017 | CADE 2017 (Gothenberg, Sweden) | Paper |
| 18-22 September 2017 | CASC 2017 (Beijing, China) | Several SC2 Papers |
| 21-24 September 2017 | SYNASC 2017 (Timisoara, Romania) | Cosortium member paper. |
| 23-24 September 2017 | PxTP 2017 (Brasilia, Brasil) | Paper |
| 27-29 September 2017 | FroCoS 2017 (Brasilia, Brasil) | Paper, Poster |
| 15-17 November 2017 | MACIS 2017 (Vienna, Austria) | SC-Square Session, co-track Chair and Papers |
| 18-22 June 2018 | ACA 2018 (Santiago de Compostela, Spain) | |
| 26-29 June 2018 | CADGME (University of Coimbra, Portugal) | |
| 3-6 July 2018 | SAT/SMT/AR Summer School 2018 (Manchester, UK) | SC-Square Sponsorship and Session |
| 16-19 July 2018 | ISSAC 2018 (New York City, USA) |
Background
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
News Archive
The vidoes of the Saarbrücken Summer School are now available here.
SC-Square held its second formal workshop in Kaiserslautern Saturday 29th July, immediately after ISSAC 2017 and before the SC2 Summer School in nearby Saarbrücken.
SC-Square held its SC2 Summer School in Saarbrücken from Monday, July 31st, to Friday, August 4th, 2017.
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 and an SC2 session at ACA 2016 in August.
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. Click here to download the SC-square Announcement Poster.
Objectives
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.- O1) Build a joint SC2 community: Build a community of researchers interested in developing technologies at the boundary of the traditionally separate areas of Satisfiability Checking and Symbolic Computation.
- O1.1) Create communication platforms: Create platforms for scientific exchange, discussion and cooperation within and between the currently disjoint communities.
- O1.2) Initiate cooperations: Support the initiation and the fostering of cooperations within and across the communities of Satisfiability Checking and Symbolic Computation.
- O1.3) Strengthen research and technology transfer to industry: Identify obstacles and enabling conditions for the application of SC2 software tools (SMT solvers and computer algebra systems) in industry, and support the initiation of collaborations between academia and industry.
- O1.4) Support scientific offspring: Increase the involvement and support of young researchers and minorities, especially women, in the SC2 network.
- O2) Create a research roadmap: Create a research roadmap of potentials and challenges, both to the two traditional silos of Satisfiability Checking and Symbolic Computation, but also challenges that only the new joined SC2 community can address.
- O2.1) Common research roadmap: Identify in detail, the research challenges that cross community boundaries, and where appropriate construct prototype proof-of-concept implementations (sufficient for handling modest, but non-trivial examples).
- O2.2) Research roadmap for Satisfiability Checking: Identify in detail, the research challenges for the Satisfiability Checking community: Identify established techniques in Symbolic Computation which are promising candidates to adapt and integrate to tackle problems arising in Satisfiability Checking, and where appropriate construct prototype proof-of-concept implementations (sufficient for handling modest, but non-trivial examples).
- O2.3) Research roadmap for Symbolic Computation: Identify in detail, the research challenges for the Symbolic Computation community: Identify successful techniques in Satisfiability Checking and generalise them to become applicable also in the area of Symbolic Computation, and where appropriate construct prototype proof-of-concept implementations (sufficient for handling modest, but non-trivial examples).
- O3) Initiate SC2 standards: Create standards and benchmark libraries such that the SC2 community can share challenges and measure its progress.
- O3.1) Propose input language standards: Develop appropriate standards for the input language of SC2 tools, such that a problem specified in the standard input language can be input to several tools.
- O3.2) Create an SC2 benchmark library: Create and disseminate a library of SC2 benchmarks in the standard input language, focussing on(linear and non-linear real and integer) arithmetic theories.
- O4) Increase the visibility of SC2: Disseminate research topics and results to other related research areas and to the public, with a special focus on young researchers and aiming at gender and geographic balance (e.g., addressing eastern Europe, surprisingly not so active in these areas).