SC-Square: Symbolic Computation and Satisfiability Checking

session at ACA 2016 to be held 1-4 August 2016 in Kassel, Germany

John Abbott (in email address please replace triple t by double t), University of Kassel, Germany

Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems. More recent developments in the area of Satisfiability Checking (especially SMT) are starting to tackle similar problems but with different algorithmic and technological solutions.

Satisfiability Checking is an essential back-end for assuring the security and the safety of computer systems. In various scientific areas, Symbolic Computation is able to deal with large mathematical problems far beyond the scope of pencil-and-paper solutions.

Currently the two communities are largely disjoint and unaware of the achievements of one another, despite there being strong reasons for them to collaborate. The SC-square project aims to build bridges between the communities unifying their strengths, stimulating cross-fertilization, and leading to the development of radically improved software tools.

If you are interested in proposing a talk (25 mins), please send an abstract to the organizers by 29 May 2016.
Please use this LaTeX template for your abstract, and send both the LaTeX source and a compiled PDF version.


Please see the pink session on Thursday (morning and afternoon) in the ACA schedule.


James Davenport+SC2 consortiumSC2: Satisfiability Checking meets Symbolic Computation
Anna BigattiImplicitization with Groebner Bases: the well known algorithm and algorithms which work
(Associated paper)
Stephen ForrestIntegration of a SAT Solver Into Maple
Other slides at ACA 2016
James DavenportWhat does "without loss of generality" mean

Go to:
ACA 2016 main page