16 May 2014
Utrecht, The Netherlands
******************************************
* *
* NVTI Theory Day May 16, 2014: *
* Programme, Abstracts, and Registration *
* *
******************************************
We are happy to invite you for the Theory Day 2014 of the
NVTI (Nederlandse Vereniging voor Theoretische Informatica,
Dutch Asssociation for Theoretical Computer Science).
The NVTI supports the study of theoretical computer science
and its applications.
NVTI Theory Day 2014
Friday May 16, 2014, 9:30-16:45
VERGADERRUIMTE UTRECHT !! PLEASE NOTE THE LOCATION !!
Pieterskerkhof 23
Utrecht
http://www.vergaderruimte-utrecht.nl/
See below for a "how to get there"
We have an interesting program, covering important streams in
theoretical computer science, with excellent speakers from
The Netherlands and abroad:
Erika Abraham (RWTH Aachen University, Germany)
http://www-i2.informatik.rwth-aachen.de/i2/eab/
Marieke Huisman (University of Twente)
http://wwwhome.ewi.utwente.nl/~marieke/
Elena Marchiori (Radboud University, Nijmegen)
http://www.cs.ru.nl/~elenam/
Peter Bro Miltersen (Aarhus University, Denmark)
http://www.daimi.au.dk/~bromille/
It is possible to participate in the organized lunch,
for which registration is required. The costs of around
15 Euro can be paid (cash) at the location. We just mention
that in the direct vicinity of the meeting room there
are plenty of nice lunch facilities as well.
It is also possible to participate in the organized dinner,
which will take place in Restaurant Luden, close to the
station, http://www.luden.nl/, around 18.00. The dinner
(meat, fish, or vegetarian) costs around 30 euro.
Both for the lunch and for the dinner:
Please register with Ms Susanne van Dam (Susanne.van.Dam@cwi.nl
or 020 592 4189) no later than Monday May 12, 2014.
The NVTI theory days are sponsored (financially or in kind) by
NWO (Netherlands Organisation for Scientific Research),
CWI (Dutch Center of Mathematics and Computer Science),
the Dutch research schools IPA (Institute for Programming Research
and Algorithmics) and SIKS (Dutch research school for Information
and Knowledge Systems), and by Elsevier Science.
Please find the full program and abstracts of the lectures below.
Kind regards,
Femke van Raamsdonk
*********************************************************************
*********************************************************************
Programme of the NVTI Theory Day of May 16, 2014
*********************************************************************
*********************************************************************
9.30-10.00: Arrival with Coffee
10.00-10.10: Opening
10.10-11.00: Speaker: Marieke Huisman (University of Twente)
Title: Verification of Concurrent Software
11.00-11.30: Coffee/Tea
11.30-12.20: Speaker: Peter Bro Miltersen (Aarhus University, Denmark)
Title: Real Algebraic Geometry in Computational Game Theory
12.20-12.40: Speaker: Joep van Wijk (NWO)
12.40-14.10: Lunch (see above for registration)
14.10-15.00: Speaker: Erika Abraham (RWTH Aachen University, Germany)
Title: Modeling and analyzing probabilistic systems
15.00-15.20: Coffee/Tea
15.20-16.10: Speaker: Elena Marchiori (Radboud University, Nijmegen)
Title: Axioms for graph clustering
16.10-16.40: Business meeting NVTI
*********************************************************************
*********************************************************************
Abstracts of the talks of NVTI Theory Day of May 16, 2014
*********************************************************************
*********************************************************************
10.10-11.00
Speaker: Marieke Huisman (University of Twente)
Title: Verification of Concurrent Software
Abstract:
This talk presents the VerCors approach to verification of concurrent
software. First we discuss why verification of concurrent software is
important, but also challenging, and then we show how permission-based
separation logic allows one to reason about multithreaded Java programs
in a thread-modular way.
We discuss in particular how we use the logic to use specify and verify
different implementations of synchronisers, and how we reason about
class invariance properties in a concurrent setting.
Further, we show how the approach is also suited to reason about programs
using a different concurrency paradigm, namely kernel programs using the
Single Instruction Multiple Data paradigm. Concretely, we illustrate how
permission-based separation logic is used to verify functional correctness
properties of OpenCL kernels.
*********************************************************************
*********************************************************************
11.30-12.20
Speaker: Peter Bro Miltersen (Aarhus University, Denmark)
Title: Real Algebraic Geometry in Computational Game Theory
Abstract:
We discuss two recent applications of Real Algebraic Geometry in
Computational Game Theory:
1) A tight worst case upper bound on the running time of the strategy
iteration algorithm for concurrent reachability games.
2) Polynomial time equivalence between approximating a Nash equilibrium
and approximating a trembling hand perfect equilibrium of a multi-player
game in strategic form.
The applications appear in joint works with Kousha Etessami, Rasmus
Ibsen-Jensen, Kristoffer Arnsfelt Hansen, Michal Koucky, Niels
Lauridsen, Troels Bjerre Soerensen and Elias Tsigaridas.
*********************************************************************
*********************************************************************
14.10-15.00
Speaker: Erika Abraham (RWTH Aachen University, Germany)
Title: Modeling and analyzing probabilistic systems
Abstract:
Many real-world applications exhibit random behavior. Prominent examples
are randomized distributed algorithms, where randomization is used to
break the symmetry between identical processes in leader election and
mutual exclusion algorithms, for routing purposes, or for obtaining
consensus---a problem that is known to be practically unsolvable in a
deterministic setting as indicated by various
results.
Prevailing formalisms to model such applications are discrete-time
Markov decision processes (MDPs) and deterministic simplifications
thereof, so-called discrete-time Markov chains (DTMCs). After
introducing these model classes, we discuss how probabilistic safety
properties can be model checked on MDP models or, more generally,
maximal probabilities of satisfying $\omega$-regular properties.
An important limitation of probabilistic model checking is the lack of
diagnostic feedback in case a property is violated. We shortly discuss
what counterexamples are in the probabilistic setting and how to
determine them algorithmically.
*********************************************************************
*********************************************************************
15.20-16.10
Speaker: Elena Marchiori (Radboud University, Nijmegen)
Title: Axioms for graph clustering
Abstract:
Cluster analysis, also called clustering, is an important topic in
machine learning, with a wide range of applications in diverse areas
such as life and biomedical sciences, sociology, and economy. A set
of objects is divided into groups in such a way that objects in one
group are more `related' to each other than to objects in the other
groups.
In spite of intense research there is no common agreement on the
definition of clustering. Consequently, different perspectives have
emerged yielding a wealth of methods. Many methods for clustering are
based on optimizing a quality function, which assigns a score to a
clustering. Clustering is then performed by optimizing such a function.
In this talk we will discuss axioms for clustering, that is, properties
that intuitively ought to be satisfied by clustering quality functions.
After a short introduction to clustering and its applications,
we will discuss these axioms. In particular, we will illustrate their
use to rule out and to improve clustering quality functions.
This is joint work with Twan van Laarhoven.
*********************************************************************
*********************************************************************
HOW TO GET TO VERGADERRUIMTE UTRECHT
*********************************************************************
*********************************************************************
Description of walking route from Utrecht CS (850 meter 10 minutes):
(translated from http://www.vergaderruimte-utrecht.nl/)
1. Go into the mall Hoog Catharijne (follow `Centrum')
and take the exit `Moreelsepark'.
(turn right after ABN AMRO en go straight on after that).
2. Pass through the revolving doors (next to HEMA)
and take the escalator downwards.
3. Once outside, turn left.
4. After approximately 300 meters
(you cross a broad street, sort of crossing twice)
until you cannot proceed further,
and almost enter a Chinese wok restaurant,
turn right.
5. After approximately 50 meters,
turn left at the first street, which is `Zadelstraat'.
Now you walk towards the Domtoren.
Continue straight on until you stand in front of the Domtoren.
6. Pass with the Domtoren on your right hand, and walk straight on.
Take the Voetiusstraat, this leads you automatically to the Pieterskerkhof.
On your left, you see a passageway with a gate (barrier).
This is the entrance to vergaderruimte.
--------------------
Looproute beschrijving vanaf Utrecht CS (850 meter 10 minuten):
(overgenomen van http://www.vergaderruimte-utrecht.nl/)
1. Loop Hoog Catharijne in (volg `Centrum') en neem uitgang `Moreelsepark'
(na de ABN AMRO rechtsaf en vervolgens rechtdoor lopen).
2. Ga door de draaideuren (naast de HEMA) en neem de roltrappen naar beneden.
3. Buiten aangekomen ga je linksaf.
4. Na ca. 300 meter (je steekt twee maal een weg over)
tot je niet meer verder kunt
en tegen een Chinees wok restaurant aanloopt ga je rechtsaf.
5. Na ca 50 meter sla je de eerste straat links in (Zadelstraat).
Je loopt nu recht op de Domtoren af.
Loop rechtdoor tot je recht voor de Domtoren staat.
6. Passeer de Domtoren aan de linkerkant en loop rechtdoor.
Via de Voetiusstraat kom je automatisch uit op het Pieterskerkhof.
Aan de linkerkant zie je een passage (doorgang) met een slagboom.
Dit is de toegang naar de vergaderruimte.