[SMT-LIB] CfP Summer School on Satisfiability Checking and Symbolic Computation

[Erika Abraham]

================================================
FIRST 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/
================================================

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.

====================
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 at 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)