[Caml-list] 4th International SAT/SMT Summer School

[Caml-list] 4th International SAT/SMT Summer School

[Geoff Sutcliffe]

===========================================
CALL FOR PARTICIPATION

Fourth International SAT/SMT Summer School
Semmering, Austria, July 10-12, 2014
http://satsmt2014.forsyte.at/
===========================================

REGISTRATION:
The registration deadline for the summer school is April 19, 2014.
Full details of the registration procedure as well as travel and
accommodation grants are available at the school website
(http://satsmt2014.forsyte.at/).

ABOUT:
Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers
have become the backbone of numerous applications in computer science,
such as automated verification, artificial intelligence, program
synthesis, security, product configuration, and many more. The summer
school covers the foundational and practical aspects of SAT and SMT
technologies and their applications.

Besides providing a well structured introduction to SAT and SMT, this
year's edition of the SAT/SMT Summer School covers timely topics and
novel applications such as

- parallel solvers,
- non-linear arithmetic in SMT,
- the IC3 model checking paradigm,
- hardware and software verification,
- proofs and Craig interpolation,
- and cryptography,

presented by distinguished speakers and experts in these fields. In
addition to the theory sessions, we will have practicals in which the
participants will work state-of-the-art tools and solvers.

The fourth edition follows the schools that took place at MIT (SAT/SMT
Solver Summer School 2011), at Fondazione Bruno Kessler (SAT/SMT
School 2012) in Trento, Italy, and Aalto University in Espoo, Finland
in 2013.  The school location and schedule has been chosen to
integrate nicely with the Vienna Summer of Logic (VSL 2014,
seehttp://vsl2014.at/). As a reminder, VSL 2014 includes, among many
other events:

* the 17th International Conference on Theory and Applications of
  Satisfiability Testing (SAT 2014)
* the 26th International Conference on Computer Aided Verification (CAV 2014)
* the 12th International Workshop on Satisfiability Modulo Theories (SMT 2014)
* the 7th International Joint Conference on Automated Reasoning (IJCAR 2014)

The Summer School program will feature four lectures per day, with the
first two days dedicated to SAT and SMT, and the last to special
topics. Two of the lectures will be organized as tutorials giving
hands-on experience on SAT/SMT-based modelling.

List of invited lectures:
* Introduction to SAT, Daniel Le Berre
* Practical Session SAT, Keijo Heljanko, Tomi Janhunen, Tommi Junttila
* Interpolation in SAT & SMT, Philipp R?mmer
* Parallel SAT Solving, Christoph Wintersteiger
* Proofs in SAT and CSP, Ofer Strichman
* Introduction to SMT, Alberto Griggio
* Non-linear Arithmetic in SMT, Leonardo de Moura
* Practical Session SMT, Keijo Heljanko, Tomi Janhunen, Tommi Junttila
* SMT for Cryptography & Software Verification, Chao Wang
* Hardware Verification with IC3, Fabio Somenzi
* Software Verification with IC3, Nikolaj Bj?rner

A more detailed program is available at the school website
(http://satsmt2014.forsyte.at/).

Organizers:
Clark Barrett (New York University)
Pascal Fontaine (Inria, Loria, University of Lorraine, France)
Dejan Jovanovi? (SRI, U.S.)
Georg Weissenbacher (TU Wien, Austria)