[ date | register | speakers | program | slides |
overview | audience | organization | accomodation | related ]
Advanced Winter School on
Reasoning Engines for Rigorous System Engineering
Preliminary schedule available (16
Registration online (15 January
Web-site online (31 December 2013)
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.
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
As local student or employee of JKU you can
register for free.
Lunch vouchers and shool dinner is not included in local
As external attendant registration cost is 100
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
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.
Armin Biere Johannes
Kepler University, Austria
Satisfiability Solving (SAT) and Lingeling
Bjorner Microsoft Research, USA
Satisfiability Modulo Theories (SMT) and Z3
Technical University of Vienna, Austria
Lonsing Technical University of Vienna, Austria
Quantified Boolean Formulas (QBF) and DepQBF
Chalmers University of Technology, Sweden
University of Manchester, UK
First-Order Theorem Proving (FO) and Vampire
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
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.
Here is a preliminary set of slides:
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.
The school is open to all members, collaborators and friends of
RiSE but also encourage other
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.
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.
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.
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