****************************************** * * * 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 +31(0)20 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), Elseviers Science, CWI (Dutch Center of Mathematics and Computer Science), and the Dutch research schools IPA (Institute for Programming Research and Algorithmics) and SIKS (Dutch research school for Information and Knowledge Systems). 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 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.