7 March 2003, NVTI Theoryday 2003

Het is ons een genoegen u uit te nodigen tot het bijwonen van de Theoriedag 2003 van de NVTI, de Nederlandse Vereniging voor Theoretische Informatica, die zich ten doel stelt de theoretische informatica te bevorderen en haar beoefening en toepassingen aan te moedigen. De Theoriedag 2003 zal gehouden worden op vrijdag 7 maart aanstaande, in Vergadercentrum Hoog Brabant te Utrecht, gelegen in winkelcenrum Hoog Catharijne, op enkele minuten loopafstand van CS Utrecht, en is een voortzetting van de reeks jaarlijkse bijeenkomsten van de NVTI die acht jaar geleden met de oprichtingsbijeenkomst begon.

Evenals vorige jaren hebben wij een aantal prominente sprekers uit binnen- en buitenland bereid gevonden deze dag gestalte te geven met voordrachten over recente en belangrijke stromingen in de theoretische informatica. Naast een wetenschappelijke inhoud heeft de dag ook een informatief gedeelte, in de vorm van een algemene vergadering waarin de meest relevante informatie over de NVTI gegeven zal worden, alsmede presentaties van de onderzoekscholen.

Lunchdeelname

Het is mogelijk aan een georganiseerde lunch deel te nemen; hiervoor is aanmelding verplicht. Dit kan per email of telefonisch bij Susanne van Dam (susanne at cwi.nl, 020-592 4189), tot een week voor de bijeenkomst (28 februari). De kosten kunnen ter plaatse voldaan worden; deze bedragen Euro 14. Wij wijzen erop dat in de onmiddellijke nabijheid van de vergaderzaal ook uitstekende lunchfaciliteiten gevonden kunnen worden, voor wie niet aan de georganiseerde lunch wenst deel te nemen.

Lidmaatschap NVTI

Aan het lidmaatschap zijn geen kosten verbonden; u krijgt de aankondigingen van de NVTI per email of anderszins toegestuurd. Wilt u lid van de NVTI worden, dan kunt u zich aanmelden bij Susanne van Dam (susanne at cwi.nl) met vermelding van de relevante gegevens (naam, voorletters, affiliatie indien van toepassing, correspondentieadres, email, URL, telefoonnummer).

Steun

De activiteiten van de NVTI worden mede mogelijk gemaakt door de ondersteuning (financieel en anderszins) van de volgende instellingen: NWO/EW, CWI, Onderzoeksscholen IPA, SIKS, OZSL, Elsevier Science B.V.

For more (english) information please email Jan Willem Klop (J.W.Klop at cwi.nl). Also please note: If you want to take part in the organised lunch (€ 14,-) you can either call or email Susanne van Dam: 020-592 4189 / susanne at cwi.nl before February 28.

---

Programme

9.30-10.00

Ontvangst met koffie

10.00-10.10

Opening

10.10-11.00

Lezing Prof.dr. L. Fortnow (Nec Laboratories America)
Church, Kolmogorov and von Neumann: Their Legacy Lives in Complexity

11.00-11.30

Koffie

11.30-12.20

Prof.dr. P. Stevenhagen (UL)
Primes is in P

12.20-12.50

Presentatie Onderzoeksscholen (OZL, IPA, SIKS)

12.50-14.10

Lunch (Zie beneden voor registratie)

14.10-15.00

Lezing Prof.dr. M. Vardi (Rice University, USA)
The Design of A Formal Property-Specification Language

15.00-15.20

Thee

15.20-16.10

Lezing Dr. M. de Rijke (UvA)
Intelligent Information Access

16.10-16.40

Algemene ledenvergadering NVTI

---

Abstracts

Prof.dr. L. Fortnow (Nec Laboratories, USA)
Church, Kolmogorov and von Neumann: Their Legacy Lives in Complexity

In the year 1903, several of the greatest early computer scientists entered our world. In this talk we look at the work of three of these giants: Alonzo Church, Andrey Kolmogorov and John von Neumann honoring the 100th anniversary of their births. We will focus on how their research has and continues to play a major role in the development of computational complexity and our understanding of what we can compute.

Alonzo Church developed the lambda-calculus, a computation model equivalent to the Turing machine. He co-developed independently with Alan Turing what we now call the Church-Turing thesis that states that every computable is computable by a Turing machine (or the lambda-calculus).

John von Neumann's work in quantum mechanics, game theory, automata theory and his development of early computers have played major roles in the development of algorithms and complexity.

We will spend most of the seminar discussing the influence of Andrey Kolmogorov, whose work on algorithmic randomness has had a more direct impact on computational complexity and certainly my own research. We will give an overview of Kolmogorov complexity and several examples of computational restricted versions of this measure have helped us better understand the nature of efficient computation.

Prof.dr. P. Stevenhagen (UL)
Primes is in P

In August 2002, the Indian computer scientists Agrawal, Kayal and Saxena proved that primality of an integer can be tested by means of a deterministic algorithm that runs in polynomial time. For several decades, this had been an outstanding problem. We discuss the importance of the result in theory and practice, and give an impression of the mathematics that goes into it.

Prof.dr. M. Vardi (Rice University, USA)
The Design of A Formal Property-Specification Language

In recent years, the need for formal specification languages is growing rapidly as the functional validation environment in semiconductor design is changing to include more and more validation engines based on formal verification technologies. In particular, the usage of Formal Equivalence Verification and Formal Property Verification is growing, new symbolic simulation engines are introduced and hybrid environments of scalar and symbolic simulators are developed. To facilitate the use of these new-generation validation engines - properties, checkers and reference models need to be developed in a formal language.

In this talk we describe the design of the ForSpec Temporal Logic (FTL), the new temporal logic of ForSpec, Intel's new formal property-specification language, which is today part of Synopsis OpenVera hardware verification language (www.open-vera.com). The key features of FTL are: it is a linear temporal logic, based on Pnueli's LTL, it enables the user to define temporal connectives over time windows, it enables the user to define regular events, which are regular sequences of Boolean events, and then relate such events via special connectives, and it contains constructs that enable the user to model multiple clock and reset signals, which is useful in the verification of globally asynchronous and locally synchronous hardware designs.

The focus of the talk is on design rationale, rather than a detailed language description.

Dr. M. de Rijke (UvA)
Intelligent Information Access

Search is one of the core topics in theoretical computer science, and online search has become a day-to-day activity for many of us. Finding keywords in a text file is easy. Using keyword search, current retrieval systems allow users to find documents that are relevant to their information needs, but most leave it to the user to extract the useful information from those documents. This leaves the (often unwilling) user with a relatively large amount of text to consume. People have questions and they need answers, not documents. There is a need for tools that reduce the amount of text one might have to read to obtain the desired information.

In this talk I review ongoing research initiatives (such as novelty detection, question answering, and XML retrieval) aimed at moving beyond traditional document retrieval, and I will try to identify theoretical issues that arise from these initiatives.