Marktoberdorf Summer School
An Advanced Study Institute of the NATO Science Committee
and the Institut für Informatik, Technische Universität München, Germany

Proof Technology and Computation
July 2
to August 10, 2003

       T. Nipkow (director)
                  O. Grumberg  (director)    
       M. Broy (co-director)
       R. L. Constable (co-director)
       H. Schwichtenberg (
       S. S. Wainer (co-director)

    Katharina Spies (secretary)


The "Marktoberdorf Summer School" is a two weeks' course for young computer scientists and mathematicians working in the field of formal systems development. The course aims at the dissemination of advanced scientific knowledge and the promotion of international contacts among scientists.

“Proof technology” is a newly established field in software engineering. It generally aims at integrating proof processing into industrial design and verification tools. The origins of this technology lie in the systematic understanding of a fully-fledged, precise notion of proof by mathematicians and logicians. Using this profound understanding computer scientists are able to implement proofs, to check and to create them automatically and to connect the concepts of proof and programs in a deep way. Via this connection proofs are used to support the development of reliable software systems. Software engineers have integrated proof processing into industrial development tools, and these implementations are now getting very efficient.

The international summer school will present the state of the art and will provide an excellent opportunity for verification and dissemination.

Participation and grants*)

Deadline for application: March 7, 2003


Robert Constable 
Information Intensive Proof Technology

Gilles Dowek 
  Proofs and Computations Integrated 

Orna Grumberg 
Model Checking 

John Harrison
Verification: Industrial Applications   

Neil Jones
Computation and Complexity 

Tobias Nipkow 
Readable Formal Proofs   

Michael Rathjen
Constructive Set and Type Theories 

Helmut Schwichtenberg
Computing with Infinite Objects 

Pawel Urzyczyn
Predicates as Types

Moshe Vardi
Automata and Logic Based Systems Design   

Stan Wainer
Proof Theoretic Complexity 

*) Previous training and experience in computer science as well as a solid background in mathematics are indispensable. The applications will be considered with due regard to a fair distribution of the 80 places available among applicants from the various countries. A letter of recommendation by the home department or institution is requested.

Applications without a letter of recommendation 
cannot be taken into consideration.

The Summer School will be held at Marktoberdorf, a small town about 100 km southwest of Munich. All students will be accommodated in the boarding house (double rooms) of the local high school, Gymnasium Marktoberdorf. Due to the limited number of rooms accompanying persons cannot be lodged in the boarding house.

The directors and the organizing committee of the Summer School do not assume any responsibility or any liability for persons participating in the meeting.

All applicants will receive notice by May 15th. Every person who is admitted to attend the Summer School as participant has to pay Euro 600,- for the living expenses (covering accommodation, breakfast, lunch, dinner, refreshments, and social events) and Euro 840,- for the participation fee (including working material - to be distributed upon arrival - and a copy of the final proceedings). An invoice to the respective amount will be sent to all participants together with a letter of acceptance. Payment of the invoice is due in advance and must be remitted to our bank account by June 30th at the very latest.

It is hoped that you can obtain support for your travel and living expenses and for the participation free from your institution or other sources in your own country. However, should this not be possible, limited funds are available for those participants who will need financial aid to cover a part of their costs.  If a support for travel expenses is granted, the amount will be reimbursed to the participant during the Summer School at Marktoberdorf by a Euro-cheque.

Please fill in your application form properly and completely.

We ensure confidentiality. Personal information will be used for the selection process only.

Feel free to contact us via e-mail
Phone: (+89) 289-17829
Fax: (+89)

Postal address:
  Institut für Informatik
  Technische Universität München
  - Summer School -
  Boltzmannstr. 3
  85748 Garching (München)