12 March 2010
Utrecht, The Netherlands
Nederlandse Vereniging voor Theoretische Informatica
====================================================
We are happy to invite you for the Theory Day 2010 of the NVTI. The
Dutch Asssociation for Theoretical Computer Science (NVTI) supports
the study of theoretical computer science and its applications.
NVTI Theory Day 2010
Friday March 12, 2010, 9:30-16:40
Hoog Brabant, Utrecht (close to Central Station)
We have an interesting program with excellent speakers from The
Netherlands and abroad, covering important streams in theoretical
computer science. Below you will find the abstracts.
Speakers:
Jan Friso Groote (TU/e)
Monika Henzinger (University of Vienna, Austria)
Georges Gonthier (Microsoft Research)
Monique Laurent (CWI, Tilburg University)
It is possible to participate in the organized lunch,
for which registration is required. Please register
with Ms Caroline Waij (cpwaij@few.vu.nl or 020-5983563)
no later than one week before the meeting (March 5, 2010).
The costs of 15 Euro can be paid at the location.
We just mention that in the direct vicinity of the meeting
room there are plenty of nice lunch facilities as well.
The NVTI theory day 2010 is 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,
NVTI secretary.
*********************************************************************
*********************************************************************
9.30-10.00: Arrival with Coffee
10.00-10.10: Opening
10.10-11.00: Speaker: Jan Friso Groote (TU/e)
Title: Parameterised Boolean Equation Systems
11.00-11.30: Coffee/Tea
11.30-12.20: Speaker: Monika Henzinger (University of Vienna, Austria)
Title: Algorithmic mechanism design
or how web search engines make money
12.20-12.40:
12.40-14.10: Lunch (see above for registration)
14.10-15.00: Speaker: Georges Gonthier (Microsoft Research)
Title: Beyond the four-colour theorem:
software engineering for mathematics
15.00-15.20: Coffee/Tea
15.20-16.10: Speaker: Monique Laurent (CWI, Tilburg University)
Title: Optimization over polynomials
with sums of squares and semidefinite programming
16.10-16.40: Business meeting NVTI
*********************************************************************
*********************************************************************
Abstracts of the talks of NVTI Theory Day of March 12, 2010
*********************************************************************
*********************************************************************
10.10-11.00
Speaker: Jan Friso Groote (TU/e)
Title: Parameterised Boolean Equation Systems
Abstract:
We use formulas of the modal mu-calculus with time and data to
express properties that behavioural models should have. In order to
verify the validity of such formulas, we translate model and formula
to a so-called Parameterised Boolean Equation System (PBES).
The formula holds iff the solution of the PBES is true. The PBES
representation is so concise that translating complex models and
complex properties is straightforward and yields relatively concise
PBESs (typically smaller than megabytes). Unfortunately, solving
large PBESs is not so straightforward.
In this talk we present PBESs and provide a number of techniques
that are known to solve them. Gauss elimination, invariants,
approximation are examples. Particularly intriguing is
the use of patterns which are very helpful in certain instances.
It is an open question whether this pattern technique can be lifted to
solve any PBES. But if so, it would clearly relate the expressiveness
of PBESs to first order logic.
*********************************************************************
*********************************************************************
11.30-12.20
Speaker: Monika Henzinger (University of Vienna, Austria)
Title: Algorithmic mechanism design
or how web search engines make money
Abstract:
This talk presents a new problem in algorithmic mechanism design,
namely how to assign bidders with potentially very different utility
functions to items. We will describe the current state of the art and
present a solution for a restricted set of utility functions. We will
also explain why the problem is very relevant to internet advertisers
and to web search engines.
*********************************************************************
*********************************************************************
14.10-15.00
Speaker: Georges Gonthier (Microsoft Research)
Title: Beyond the four-colour theorem:
software engineering for mathematics
Abstract:
While the use of proof assistants has been picking up in computer science,
they have yet to become popular in traditional mathematics. Perhaps this is
because their main function, checking proofs down to their finest details,
is at odds with mathematical practice, which ignores or defers details in
order to apply and combine abstractions in creative and elegant ways. This
mismatch parallels that between software requirements and implementation.
In this talk we will explore how software engineering techniques like
component-based design can be transposed to formal logic and help bridge the
gap between rigor and abstraction, and show how these techniques were
instrumental in carrying out a fully formal proof of the famous four-colour
theorem.
*********************************************************************
*********************************************************************
15.20-16.10
Speaker: Monique Laurent (CWI, Tilburg University)
Title: Optimization over polynomials
with sums of squares and semidefinite programming
Abstract:
Polynomial optimization deals with the problem of minimizing
a multivariate polynomial over a feasible region defined by
polynomial inequalities. While polynomial time solvable when
all polynomials are linear (via linear programming), the
problem becomes hard in general as soon as it involves non-linear
polynomials. Just adding the simple quadratic constraints
x_i^2 = x_ii on the variables, already makes the problem
NP-hard as this models e.g. hard combinatorial problems like Max-Cut
or Max-Clique in graphs.
A natural approach is to consider easier to solve, convex relaxations.
The basic idea, which goes back to work of Hilbert, is to relax
non-negative polynomials (which are hard to recognize) by sums of
squares of polynomials, a notion which can be tested efficiently
using semidefinite programming algorithms. In this way hierarchies
of efficient convex relaxations can be build. We will present their
main properties. In particular, convergence properties (that rely on
real algebraic geometry representation results for positive polynomials),
stopping criteria and extraction of global minimizers (that rely on
results from the dual moment theory and commutative algebra), error
bounds in some special instances (e.g. optimization over the simplex
or the hypercube), application to computing the real solutions to
polynomial equations.