The proceedings are available.
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.30||Peter Schmitt & Bernhard Beckert, University of Karlsruhe, Germany|
``KeY, a new tool for the specification and verification of software.''
|11.30-12.30||Jozef Hooman, Nijmegen University, Holland|
``Verification of concurrency control protocols with PVS''
|14.00-14.30||Pieter Audenaert, University of Gent, Belgium|
``Memory modeling in PVS''
|14.30-15.00||Freek Wiedijk, Nijmegen University, Holland|
``Mizar, a not very well known proof tool''
|15.30-16.00||Dirk Van Heule, University of Gent, Belgium|
``Three-valued logic and Isabelle: the problems.''
|16.00-16.30||Olga Caprotti & Martijn Oostdijk, Technische Universiteit Eindhoven, Holland|
``How to formally and efficiently prove primality of large numbers''
The dinner will take place in a typical Ghent restaurant.
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).