================================================ FINAL CALL FOR PARTICIPATION First International Summer School on Satisfiability Checking and Symbolic Computation July 31 - August 04, 2017 Saarbruecken, Germany Application deadline: June 01, 2017 Notification deadline: June 15, 2017 For detailed information on the school's aim, program and the application procedure see http://www.sc-square.org/CSA/school/ *** REGISTER SOON FOR FREE ACCOMMODATION *** ================================================ The school introduces graduate students and researchers from academia and industry into research and methodology in both Satisfiability Checking (SAT/SMT) and Symbolic Computation with one focus on their interconnections. It combines a thorough introduction into the theory of both fields with lectures on state-of-the-art software systems and their implementation. This is supplemented with presentations by lecturers from industry discussing the practical relevance of the topics of the school. This project has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689. Participation is free of charge. There is a limited number of free shared rooms available for distribution by the selection committee. Please express your interest with your application. Travel costs cannot be covered by the school. ================================================ Keynote Speakers (joint with VTSA Summer School) ================================================ Rajeev Alur, University of Pennsylvania Hoon Hong, North Carolina State University ==================== Speakers and courses ==================== ---Satisfiability Checking--- Marijn Heule (University of Texas, Austin, USA) State-of-the-art SAT Solving Cesare Tinelli (University of Iowa, Iowa City, USA) Foundations of Satisfiability Modulo Theories Keijo Heljanko, Tomi Janhunen, Tommi Junttila (Aalto University, Helsinki, Finland) Practical Session on SAT/SMT ---Symbolic Computation--- Hoon Hong (North Carolina State University, Raleigh, USA) Symbolic Computation (Quantifier Elimination) James Davenport (University of Bath, United Kingdom) Symbolic Computation through Maple and Reduce Christopher W. Brown (United States Naval Academy, Annapolis, USA) Cylindrical Algebraic Decomposition and Real Polynomial Constraints ---Industrial Applications--- Tom Bienmueller (BTC Embedded Systems, Oldenburg, Germany) Industrial Applications and Challenges for Verifying Reactive Embedded Software David Deharbe (ClearSy, Aix-en-Provence, France) Formal Verification in an Industrial Setting Grant Passmore (Aesthetic Integration, London, United Kingdom) Formal Verification of Financial Algorithms ---Beyond Satisfiability Checking--- Christoph Weidenbach (MPI for Informatics, Saarbruecken, Germany) State-of-the-art FOL Solving Jasmin Blanchette (Vrije Universiteit Amsterdam, The Netherlands) Interactive Theorem Proving in Higher-Order Logics =========== Application =========== To apply for participation, please send an email to haniel.barbosa@inria.fr with the following documents: - a one page curriculum vitae, - an application letter explaining your interest in the school and your experience in the area, - a copy of a certificate of you highest academic degree (at least Bachelor or equivalent), - a support letter by a current advisor. Application deadline is June 01, 2017. Notifications on acceptance/rejection will be given by June 15, 2017. ========== Organisers ========== Erika Abraham (RWTH Aachen University, Germany) Thomas Sturm (CNRS, France and MPI Informatics, Germany)