SAT Conference: 17th International Conference on Theory and Applications of Satisfiability Testing

Uwe Egly co-chairs 17th International Conference on Theory and Applications of Satisfiability Testing which is collocated with Vienna Summer of Logic.

For more information visit http://baldur.iti.kit.edu/sat2014/.

CAV 2014 Worshops: SYNT, FRIDA, iPRA, QBF, Vampire

Collocated with CAV 2014 Conference are the workshops organized by our researchers: 

26th CAV Conference in Vienna, 18-22 July 2014

Armin Biere and Roderick Bloem are organizing the 26th Computer Aided Verification this year in Vienna.
Visit http://cavconference.org/ for more information.

Austrian Computer Science Day, June 6 2014

Roderick Bloem and Helmut Veith are co-organizing the Austrian Computer Science Day 2014.
information

7th Interaction and Concurrency Experience ICE 2014, 6th of June

Ana Sokolova co-chairs 7th Workshop Interaction and Concurrency Experience (ICE) held in Berlin.
http://www.discotec.org/workshops/ice-2014

Competitions during Vienna Summer of Logic, July 2014

Our researchers organize several competitions co-located with Vienna Summer of Logic!

  • Martina Seidl co-organizes QBF Gallery, the competition of QBF Solvers
  • Swen Jacobs co-organizes SYNTCOMP, the competition in automatic synthesis of reactive systems
  • Armin Biere co-organizes the 7th HWMCC, hardware model checking competition

4th International SAT/SMT Summer School, Semmering, Austria, July 10-12, 2014

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, see http://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)

Joint ExCAPE-ARiSE meeting on Synthesis at Berkeley

ExCAPE (Expeditions in Computer Augmented Program Engineering) project aims to transform the way we program and build a software.

ARiSE meets with ExCAPE in Berkeley to discuss the collaboration within hardware-software synthesis and verification.

RiSE Winter School 2014: Reasoning Engines for Rigorous System Engineering

Speakers: Armin Biere, Nikolaj Bjorner, Uwe Egly, Florian Lonsing, Laura Kovacs, Andrei Voronkov.

Find more information on school page.

Workshop “Theoretical Foundations of Applied SAT Solving”, Jan 19-24, Canada

Armin Biere co-organizes the unusual workshop, titled “Theoretical Foundations of Applied SAT Solving”, held in Canada.
The objective is to fill “the gap between the impressive progress on the engineering side and very slow progress on the theory side” (source).
Videos, presentations and more can be found at http://www.birs.ca/events/2014/5-day-workshops/14w5101/