SC2 2016

                     First Workshop on
    Satisfiability Checking and Symbolic Computation
                FETOPEN-CSA SC2 Workshop 1
        Bridging Two Communities to Solve Real Problems

                        September 24, 2016

Affiliated with the 18th International Symposium on Symbolic and
  Numeric Algorithms for Scientific Computing (SYNASC 2016)
                       Timisoara, Romania


              http://www.sc-square.org/CSA/workshop1.html
Preface
This volume contains the papers presented at the First Workshop on Satisfiability 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 Algo-
rithms for Scientific 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 Satisfiability Checking
are starting to tackle similar problems but with different 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 Satisfiability Checking and
Symbolic Computation together. More specifically, some suggested topics were:

   • Decision procedures and their embedding into SMT solvers and computer algebra systems
   • Satisfiability Checking for Symbolic Computation
   • Symbolic Computation for Satisfiability Checking
   • Applications relying on both Symbolic Computation and Satisfiability Checking
   • Combination of Symbolic Computation and Satisfiability Checking tools

    The workshop received ten submissions. Each submission was reviewed by at least three pro-
gram 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: satisfia-
bility 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.




September 2016


                                         Erika Ábrahám and Pascal Fontaine (Workshop Chairs)
                 James H. Davenport (SC2 H2020 FETOPEN CSA Coordinator, project 712689)


                                                II
Program Committee
John Abbott (Universität Kassel, Germany)
Bernd Becker (Albert-Ludwigs-Universität, Freiburg, Germany)
Anna M. Bigatti (Universita degli studi di Genova, Italy)
Martin Brain (University of Oxford, U.K.)
Bruno Buchberger (Johannes Kepler Universität, 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 (Universität 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)


External reviewers
Martin Bromberger (Max-Planck-Institut für Informatik, Saarbrücken, Germany)
Vladimir Gerdt (Joint Institute for Nuclear Research, Dubna, Russia)
Felix Neubauer (Albert-Ludwigs-Universität, Freiburg, Germany)
Karsten Scheibler (Albert-Ludwigs-Universität, Freiburg, Germany)




                                             III
Table of Contents
CoCoA and CoCoALib: Fast Prototyping and Flexible C++ Library for Computations in Com-
mutative Algebra
    John Abbott and Anna Maria Bigatti

Satisfaction Meets Practice and Confidence
     Tom Bienmüller and Tino Teige

Algebraic Techniques in Software Verification : Challenges and Opportunities
    Martin Brain, Daniel Kroening and Ryan McCleeary

MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
   Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias Kotsireas, Saeed Nejati
   and Krzysztof Czarnecki

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

Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving
    Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige,
    Tom Bienmüller and Detlef Fehrer




                                              IV