[  date | register | speakers | program | slides | overview | audience | organization | accomodation | related ]

News

Preliminary schedule available (16 January 2014)

Registration online (15 January 2014)

Web-site online (31 December 2013)

Date

The shool will take place from Monday to Friday of the first week in February 2014, February 3-7, 2014, at the Johannes Kepler University, in Linz, Austria, lecture room HS 19 Computer Science Building, Science Park 3.

Registration

Since the number of attendees is limited, registration is mandatory, even if you do not plan to attend all lectures. Even though we prefer early registration it is possible to register onsite before the lectures starts too. There are two types of registration options.

As local student or employee of JKU you can register for free.
Lunch vouchers and shool dinner is not included in local registration.

As external attendant registration cost is 100 Euro.
This includes lunch vouchers and the school dinner.

In order to register, send an email to our secretary Doris Falb mentioning the registration type (local or external). In case of external registration, transfer in parallel the amount of 100 Euro to the following bank account. Make sure that the money reaches us as early as possible and not later than January 27.

Institutskassa, Stichwort ReRiSE'14
IBAN: AT57 3400 0000 3182 7173
BIC: RZOOAT2L

BST Universität
Raiffeisenlandesbank Oberösterreich
4040 Linz, Altenberger Straße 69

Please make sure that the (electronic) transfer mentions your name, such that we can connect it to your registration mail, which should also contain your affiliation beside your name and if necessary dietary restrictions for the conference dinner and whether you intend to attend the dinner or not.

Note that attending members of RiSE are considered external as long as registration is concerned and have to pay the external registration cost of 100 Euro.

Speakers

Armin Biere Johannes Kepler University, Austria
Satisfiability Solving (SAT) and Lingeling

Nikolaj Bjorner Microsoft Research, USA
Satisfiability Modulo Theories (SMT) and Z3

Uwe Egly Technical University of Vienna, Austria
Florian Lonsing Technical University of Vienna, Austria
Quantified Boolean Formulas (QBF) and DepQBF

Laura Kovacs Chalmers University of Technology, Sweden
Andrei Voronkov University of Manchester, UK
First-Order Theorem Proving (FO) and Vampire

Program

The plan is to have 1.5 hour lectures on each of the four topics every day, except for Friday where we want to discuss implementation details and will review tool usage, API's and source code.

Here is a preliminary schedule.

The "hands-on" part on Friday takes place in a different building close by (Mechatronic Building, Science Park 1, MT 127). The SAT and QBF part swapped time slots on the last day, but otherwise the schedule is the same. There was a winter school dinner on Wednesday early evening.

Slides

Here is a preliminary set of slides:

• For the SAT part we use one slide set for the first four days, which related to our advanced model checking course. Additional material for the last day are the TPTPA'11 slides as well the source code of Cleaneling, PicoSAT and Lingeling.
• For the SMT part we have slides of the first, second, third, and fourth/last day.
• For the QBF part there are four separate sets of slides available for first, second, third+fourth, and lasth day.
• The FO slides of first to third day are available as one slide set.

Overview

The ReRiSE'14 winter school is an event of the Austrian national research network RiSE.

The school is about reasoning engines for rigourous system engineering and consists of lectures on principles of decision procedures, including fundamentals, state-of-art algorithms and data structures, as well as implementation techniques.

The emphasis is on techniques which are important for practical applications and used in rigorous system engineering.

Audience

The school is open to all members, collaborators and friends of RiSE but also encourage other participation too.

The target audience are users of decision procedures, and particularly researchers, such as PhD students, Post-Docs, or advances master-students working on theoretical and practical aspects of decision procedures.

Organization

The local organization including registration is handled by the Institute of Formal Models and Verification of the Johannes Kepler University, in Linz, Austria.

This course is eligible for students of JKU and can be credited as an instance of the advanced model checking course. In order to obtain credits an oral exam is required. Please contact Armin Biere if you are interested in this option.

Accomodation

There are very few opportunities in walking distance, particularly since we were told that Sommerhaus hotel is close to being booked out. So you probably will need to find a hotel in the city center, which is 15 minutes away by tram. Check your favorite hotel online platform for available options.

Related

The related event AAA87 & CYA28 will take place on the weekend after the winter school, overlapping with the winnter school by one day on Friday. We encourage attendees of both events to take part in the other as well and are working on a model to allow registered attendees of one event to attend the other for free.