http://www.sc-square.org/CSA/workshop2.html
Matthew England1 and Vijay Ganesh2
Coventry University, Coventry, UK Matthew.England@coventry.ac.uk,
University of Waterloo, Canada
vganesh@uwaterloo.ca,
This volume contains the papers presented at the Second International Workshop on Satis ability Checking and Symbolic Computation (SC2 2017). The workshop was held on the 29th July 2017 at the University of Kaiserslautern in Kaiserslautern, Rheinland-Pfalz, Germany.
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 have rarely interacted until recently. 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 SC2 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 SC2 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 Symbolic Computation and Satis ability Checking { Combination of Symbolic Computation and Satis ability Checking tools
This is the second SC2 workshop: the rst took place in September 2016 in Timisoara, Romania3 with proceedings available as Volume 1804 of CEUR-WS4.
The workshop solicited submissions to the proceedings as either full papers or extended abstracts. In either case each of these submissions received at least three reviews from the program committee members. We accepted 3 full papers and 4 extended abstracts into these CEUR-WS proceedings.
Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving { Martin Brain, James H. Davenport and Alberto Griggio - Benchmarking
Solvers, SAT-style Extended Abstracts: { Rui-Juan Jing and Marc Moreno Maza - Computing the Integer Points of a
Polyhedron { Erika Abraham, Jasper Nalbach and Gereon Kremer - Embedding the Virtual Substitution Method in the Model Constructing Satis ability Calculus Framework { John Abbott and Anna Maria Bigatti - New in CoCoA-5.2.0 and CoCoALib0.99550 for SC-Square { Stephen Forrest - Integration of SMT-LIB support into Maple
In addition, the workshop solicited presentations without publication on topics of work that had been published elsewhere but would be of interest to the SC2 community. These contributions were assessed for relevance by the program committee with 5 such presentation taking place at the workshops. Presentations without Publication: { Maximilian Jaroschek, Andreas Humenberger and Laura Kovacs - Polynomial Invariant Generation for Multi-Path Loops { Daniela Ritirc, Armin Biere and Manuel Kauers - Complexity of circuit ideal membership testing { Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm and Xuan Tung Vu - Subtropical Satis ability { Martin Bromberger and Christoph Weidenbach - Computing a Complete
Basis for Equalities Implied by a System of LRA Constraints { Curtis Bright, Ilias Kotsireas and Vijay Ganesh - A SAT+CAS Method for
Enumerating Williamson Matrices of Even Order { Deepak Kapur - Nonlinear Polynomials, Interpolants and Invariant Generation for System Analysis The last of these was a survey of work and the chairs agreed to include a nonreviewed survey paper into the proceedings as a useful reference for participants.
The workshop had an invited talk, by Jeremy Avigad (Carnegie Mellon University) on The Lean Theorem Prover.
Abstract: Lean is a new interactive theorem prover that is based on dependent type theory. The system is designed to combine interactive theorem proving, computation, and automation within the same logical framework. Dependent type theory provides an expressive language for reasoning about concrete and abstract mathematical structures, and the fact that it has a computational interpretation means that Lean can be used as a programming language as well. With a suitable interface to the system internals, it can also be used as a metaprogramming language, that is, a language with which one can extend the functionality of the system itself. I will survey all these aspects of the system in this talk, and consider ways that Lean can be used as a platform to unify symbolic combination, automated reasoning, and veri ed proof. In particular, I will describe a Lean-Mathematica connection developed by Robert Y. Lewis, which takes advantage of Lean's metaprogramming capabilities.
{ Matthew England (Coventry University, U.K.) { Vijay Ganesh (University of Waterloo, Canada) Program Committee { Erika Abraham (RWTH Aachen University, Germany) { Jeremy Avigad (Carnegie Mellon University, USA) { Anna M. Bigatti (Universita degli studi di Genova, Italy) { James H. Davenport (University of Bath, U.K.) { Pascal Fontaine (Universite de Lorraine, Inria, Loria, Nancy, France) { Stephen Forrest (Maplesoft) { Mark Giesbrecht (University of Waterloo, Canada) { Alberto Griggio (Fondazione Bruno Kessler, Trento, Italy) { Dejan Jovanovic (SRI, USA) { Ilias Kotsireas (Wilfrid Laurier University, Canada) { Daniel Kroening (University of Oxford, U.K.) { Felix Neubauer (University of Freiburg, Germany) { Grant Olney Passmore (Aesthic Integration, U.K.) { Werner Seiler (Universitat Kassel, Germany) { Thomas Sturm (CNRS, Nancy, France and MPI Informatik, Germany) { Wolfgang Windsteiger (Johannes Kepler Universitat, Linz, Austria) The Co-Chairs would like to thank all authors and participants of the workshop for helping make this a successful event. Our particular thanks go to the Program Committee for their helpful and detailed reviews.
We used the Easychair Conference System software to manage the submission and reviewing procedures and are grateful to the Easychair team for this service. The proceedings are published using CEUR-WS, and we thank all the people and institutions that make CEUR proceedings possible.
The main costs of the event were met by the SC2 project which is funded under the European Union's Horizon 2020 research and innovation programme, grant agreement No H2020-FETOPEN-2015-CSA 712689. We are also grateful to the University of Kaiserslautern for hosting the event, and in particular extend our thanks to Local Organiser Claus Fieker.