John Abbott Alberto Griggio 0 1 2 3 4 5 6 7 Program Committee David Monniaux, University of Grenoble , France Erika Abraham, RWTH Aachen University , Germany John Abbott, University of Passau , Germany, co-chair Konstantin Korovin, University of Manchester , UK Laura Kovacs , TU Wien , Austria Martin Brain, University of Oxford , UK Stefan Ratschan, Academy of Sciences of the Czech Republic , Prague , Czech Republic Thomas Sturm, CNRS, Nancy , France and MPI Informatik , Germany 2019

This volume contains the papers presented at the 4-th Workshop on Satis ability Checking and Symbolic Computation (SC-square) held on 10th July 2019 in Bern (Switzerland) as part of the SIAM Conference on Applied Algebraic Geometry, SIAM AG 2019. This workshop continues the series founded during the SC-Square project: project number 712689 under the auspices of H2020 FETOPEN Coordination and Support Activity. The project's goal was to bring together two communities, namely Symbolic Computation and SAT/SMT Satis ability Checking, to bene t mutually through shared knowledge and experience, and to build bridges enabling future fruitful collaboration. The Symbolic Computation community is concerned with nding algorithms that can compute exact solutions to quite general and complex mathematical problems. The approach is rmly grounded in mathematics, and particularly in computational algebraic geometry. Combining techniques from many elds including modern algebra, geometry and analysis, they represent the state-of-the-art in mathematical insight into real-valued polynomial problems. Conversely, the SAT/SMT community takes a strongly practical approach to solving a variety of logical problems arising from the veri cation and synthesis of computer hardware and software. More recently attention has been turned to supporting \algebraic theories" such as reasoning over real and oating-point numbers. This is driven by a desire to apply SMT techniques in ever wider elds. These two communities have numerous interests in common, such as providing capable, e cient, scalable and exible tools for solving a variety of mathematical, engineering and computation problems. However, until the SC-Square Project they were largely oblivious of one another. This project has brought them together, and in these proceedings we see some of the early fruits of this new-found collaboration, and hints to future directions where joint understanding will hopefully lead to startling progress. The Workshop chairs would like to thank the members of the Programme Committee, the authors and all the participants who made the workshop so interesting, productive and stimulating.