http://www.sc-square.org/CSA/workshop1.html This volume contains the papers presented at the First Workshop on Satis ability Checking and Symbolic Computation (SC2 2016). The workshop was held on September 24, 2016, in Timisoara, Romania, in association with the 18th International Symposium on Symbolic and Numeric Algorithms for Scienti c Computing (SYNASC 2016).
Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems; more recent developments in the area of Satis ability Checking are starting to tackle similar problems but with di erent algorithmic and technological solutions. The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible tool interfaces is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop, along the SC-square H2020 FETOPEN Coordination and Support Activity project (712689), was to provide a time to discuss, share knowledge and experience across both communities.
The workshop was open for submission and participation to everyone interested in the topics, whether they were members or associates of the SC-square H2020 FETOPEN CSA project or not.
Papers were solicited on topics that include all aspects involving Satis ability Checking and Symbolic Computation together. More speci cally, some suggested topics were: Decision procedures and their embedding into SMT solvers and computer algebra systems Satis ability Checking for Symbolic Computation Symbolic Computation for Satis ability Checking Applications relying on both Symbolic Computation and Satis ability Checking Combination of Symbolic Computation and Satis ability Checking tools
The workshop received ten submissions. Each submission was reviewed by at least three program committee members, and nine papers were accepted for presentation at the workshop and inclusion in the informal proceedings. Seven papers are included in these CEUR proceedings, according to the wishes of the authors. The workshop had an invited talk, by Christopher W. Brown (United States Naval Academy, USA) on the topic \Real polynomial constraints: satis ability checking brings a new perspective to symbolic computing".
The workshop organizers would like to thank the authors and participants of the workshop for helping making this a successful event. Our particular thanks go to the program committee and the external reviewers for their reviewing work. We are also grateful to the SYNASC organizers for their support and for hosting the workshop, and are indebted to the EasyChair team for the availability of the EasyChair Conference System. The proceedings are published under CEUR, and we would like to warmly thank all the people and institutions that make CEUR proceedings possible.
James H. Davenport (SC2 H2020 FETOPEN CSA Coordinator, project 712689) II
John Abbott (Universitat Kassel, Germany) Bernd Becker (Albert-Ludwigs-Universitat, Freiburg, Germany) Anna M. Bigatti (Universita degli studi di Genova, Italy) Martin Brain (University of Oxford, U.K.) Bruno Buchberger (Johannes Kepler Universitat, Linz, Austria) Changbo Chen (Chinese Academy of Sciences, China) James H. Davenport (University of Bath, U.K.) Matthew England (Coventry University, U.K.) Stephen Forrest (Maplesoft Europe Ltd) Vijay Ganesh (University of Waterloo, Canada) Alberto Griggio (Fondazione Bruno Kessler, Trento, Italy) Daniel Kroening (University of Oxford, U.K.) Werner Seiler (Universitat Kassel, Germany) Thomas Sturm (CNRS, Nancy, France and MPI Informatik, Germany) Cesare Tinelli (The University of Iowa, USA) Ashish Tiwari (SRI, Menlo Park, CA, USA)
Martin Bromberger (Max-Planck-Institut fur Informatik, Saarbrucken, Germany) Vladimir Gerdt (Joint Institute for Nuclear Research, Dubna, Russia) Felix Neubauer (Albert-Ludwigs-Universitat, Freiburg, Germany) Karsten Scheibler (Albert-Ludwigs-Universitat, Freiburg, Germany)
III CoCoA and CoCoALib: Fast Prototyping and Flexible C++ Library for Computations in Commutative Algebra
John Abbott and Anna Maria Bigatti Satisfaction Meets Practice and Con dence
Tom Bienmuller and Tino Teige Algebraic Techniques in Software Veri cation : Challenges and Opportunities
Martin Brain, Daniel Kroening and Ryan McCleeary What does \without loss of generality" mean (and how do we detect it)
James H. Davenport Experience with Heuristics, Benchmarks & Standards for Cylindrical Algebraic Decomposition
Matthew England and James H. Davenport