Organisational Things

• Workshop Place: The workshop will take place on the Campus of the Saarland University ( interactive map ) in Building 36.1 , 4 ^th floor, Room 407 .
• Call for Participation

• Registration: The registration is free and includes the two lunches and – depending on how much funding we can find – also the social diner on Thursday evening.

  Please register until November 5^th 2004 by sending an e-mail to Serge Autexier.

• Traveling and Hotels: Traveling information to the University Campus ( interactive map ) Saarbrücken can be found here . A selection of hotels as well as a link to the Saarbrücken Tourist's office can be found here .
• Contact: Serge Autexier for Saarbrücken and Frédéric Blanqui for Nancy

• Here are some pictures.

Participants+Talks

Program

Thursday, November 25^th 2004

10:15 - 10:30

Jörg Siekmann (Saarland University & DFKI): Welcome & Introduction

10:30 - 12:30

Session 1: Software Verification

10:30 - 11:10

Dominique Cansell, Dominique Méry, Cyril Proch (LORIA, Nancy): Proof-based development of Systems on Chip

11:10 - 11:50

Carsten Ihlemann (MPI, Saarbrücken): Processor Datapath VErification with SPASS

11:50 - 12:30

Mohamed Nassim Seghir (MPI, Saarbrücken): Software Model Checking of C program

12:30 - 14:00

Lunch

14:00 - 16:00

Session 2: Formal Software Development

14:00 - 14:40

Stephan Merz (LORIA, Nancy): Specification and Refinement of Mobile Systems in MTLA

14:40 - 15:20

Abdessamad Imine (LORIA, Nancy): Deductive Verification of Distributed Groupware Systems

15:20 - 16:00

Lassaad Cheikhrouhou, Georg Rock, Werner Stephan (DFKI Saarbrücken): VSE

16:00 - 16:30

Coffee Break

16:30 - 18:30

Session 3: Deduction I

16:30 - 17:10

Frédéric Blanqui (LORIA, Nancy): Size-based Termination

17:10 - 17:50

Jean-Yves Marion (LORIA, Nancy): Complexity and Ressource Control

17:50 - 18:30

Chad Brown (Saarland University, Saarbrücken): Automated Theorem Proving in Extensional Type Theory

20:00

Workshop Dinner at the restaurant Horch , Mainzer Str. 2, 66111 Saarbrücken ( Map )

Friday, November 26^th 2004

9:00 - 11:00

Session 4: Deduction II

9:00 - 9:40

Claude Kirchner (LORIA, Nancy): Abstract Saturation-based Inference

9:40 - 10:20

Pascal Fontaine (LORIA, Nancy): Decision procedures for unquantified first-order logic with theories

10:20 - 11:00

Virgile Prevosto (MPI Saarbrücken): ModuProve: A modular and parametric SAT-checker

11:00 - 11:20

Coffee Break

11:20 - 12:40

Session 5: E-Learning

11:20 - 12:00

Erica Melis (DFKI , Saarbrücken): The ActiveMath Learning Environment + Demo

12:00 - 12:40

Matthieu Quignard (LORIA, Nancy): DREW : collaborative argumentation graphs for learning a debate

12:40 - 14:00

Lunch

14:00 - 16:00

Session 6:

14:00 - 14:40

Christoph Benzmüller, Martin Pollet (Saarland University, Saarbrücken): The Mathematical Proof Assistance System Ωmega + Demo

14:40 - 15:20

Andreas Meier (DFKI, Saarbrücken): Proof-Planning with Multiple-Strategies

15:20 - 16:00

16:00 - 16:30

Discussion