[TYPES/announce] Summer School on Satisfiability Checking and Symbolic Computation

[Pascal Fontaine]

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