Universiteit Gent Instituut voor Programmatuurkunde en Algoritmiek

Fifth Dutch Proof Tool Day

University of Ghent

Location: Galglaan 2

May 26, 2000

The proceedings are available.

General information

The "Fifth Dutch Proof Tools Day" organized by Formosa and ProTaGoNist/IPA is the successor of the meeting held at Eindhoven University of Technology May 25, 1999.

Formosa (Formally Validated Thread Generation for Multithreaded Operating Systems), is a project in the framework of a concerted research action (GOA) of the University Gent (Belgium) where proof tools are used for proving the correctness of formal specifications of memory models for concurrent processes.

ProTaGoNist is a group of people from the Netherlands working with proof tools. Within the Dutch Graduate School IPA, the Institute for Programming research and Algorithmics, several research groups are participating with a strong interest in theorem proving and proof checking, and in the application of this technology for proving the correctness of programs, protocols and the formalization of mathematical reasoning in general.

The day will consist of a number of talks on different proof tools and their uses, and a discussion. ProTaGoNist also aims at improving the informal relations between people working in the field of theorem proving. Therefore, the day will be concluded with drinks and a dinner.


10.30-11.30Peter Schmitt & Bernhard Beckert, University of Karlsruhe, Germany
``KeY, a new tool for the specification and verification of software.''
11.30-12.30Jozef Hooman, Nijmegen University, Holland
``Verification of concurrency control protocols with PVS''
14.00-14.30Pieter Audenaert, University of Gent, Belgium
``Memory modeling in PVS''
14.30-15.00Freek Wiedijk, Nijmegen University, Holland
``Mizar, a not very well known proof tool''
15.30-16.00Dirk Van Heule, University of Gent, Belgium
``Three-valued logic and Isabelle: the problems.''
16.00-16.30Olga Caprotti & Martijn Oostdijk, Technische Universiteit Eindhoven, Holland
``How to formally and efficiently prove primality of large numbers''


The event will take place at the University of Ghent, campus De Sterre, Galglaan 2 (building S22), 9000 Gent, Belgium.
A map is available.

The dinner will take place in a typical Ghent restaurant.

Registration & payment

To participate, send an e-mail specifying your name, and whether you want to join the dinner or not to dvh@cage.rug.ac.be. Please register before May 15th.
The participation fee is 800 BEF (20 Euro). The dinner costs a supplementary 1000 BEF (25 Euro). Fees are to be paid cash during the registration (9.45--10.25).

If you want to spend the night in Ghent, please let us know as soon as possible. Typical prices are in the range of 2500--3000 BEF (60--75 Euro).

More info

For specific information regarding the program, email Dirk Van Heule or phone the secretary at (+32)9/264.49.12.