*********************************************************************
*********************************************************************
       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.