9th CLAM - INKA - OMRS Workshop

20.3. - 21.3 2000, Schloss Dagstuhl

Workshop:

The CLAM-INKA-OMRS workshop (CIAO-2000) will be held in Dagstuhl from the 20th to the 21st March 2000. It is intended to provide a snapshot of research into automating mathematical reasoning, especially in the areas of proof planning, rippling and related areas. Given the widening interested in these areas, the CIAO-2000 workshop is inviting participation from groups involved in closely related research.

Information about the previous workshop is available at http://www.dai.ed.ac.uk/group/tw/ciao99

Location:

The workshop will be held at Schloss Dagstuhl. Information how to get to Dagstuhl can be obtained at the local web-side http://www.dagstuhl.de .

Timetable:

Sunday 19th:

Arrival in the afternoon (after 3:00 PM) and informal gathering in the evening.

Monday 20th
9.30 - 12.00	Verification
	Serge Autexier:	Supporting Evolutionary Formal Software Development
	Louise Dennis:	Embedding Verification in Microsoft Excel
	Heiko Mantel:	A Case Study in the Mechanical Verification of Fault Tolerance
	Axel Schairer:	Towards Incrementally Constructing Correct Code
12.00 - 13.30	Lunch
13.30 - 15.30	Integration Techniques
	Alessandro Armando:	RDL: Rewrite and Decision Procedure Laboratory
	Silvio Ranise:	A Practical Extension Mechanism for Decision Procedures
	Daniele Zini:	The Logic Broker Architecture
	Christoph Benzmueller:	Proof-Planning Based on a Multi-Agent Architecture
15.30 - 16.00	Coffee Break
16.30 - 18.00	Proof Planning
	Andreas Meier:	Proof Planning with Multiple Strategies
	Andrew Ireland:	Future of Proof Planning (discussion)
Tuesday 21st
9.30 - 12.00	Induction
	Alan Bundy:	On the psychological validity of induction
	Dieter Hutter:	Proving the correctness of abstractions by induction
	Ewen Maclean:	Generalisation as a critic to the induction strategy
	Christoph Walther:	The VeriFun System
12.00 - 13.30	Lunch
13.30 - 15.30	Misc.
	David Basin:	Reflective Metalogical Frameworks
	Dirk Stefan Schweitzer:	Transformation of Tail-Recursive Functions
	David Anatoli:	???
	Business Meeting
15.30	End of workshop	Farewell - Organizing transport to railway stations

Abstracts of Talks

can be found on this page.

Participants:

Alessandro Armando, University of Genova, talk, (So - Tu)
Serge Autexier, Saarland University, talk, (So - Tu)
David Basin, University of Freiburg, talk, (Sa - Tu)
Matthias Bormann, TU Darmstadt, (So - Tu)
Alan Bundy, University of Edinburgh, talk, (Sa - Tu)
Christoph Benzmueller, Birmingham University, talk, (So - Tu)
Claudio Castellini, University of Edinburgh, (Sa - Tu)
Anatoli Degtyarev, Manchester University, talk, (So - Wed)
Louise Dennis, University of Edinburgh, talk, (Sa - Tu)
Jeremy Gow, University of Edinburgh, (Sa - Tu)
Dieter Hutter, DFKI Saarbruecken, talk, (Sa - Tu)
Andrew Ireland, Heriot-Watt University, Edinburgh, discussion, (Sa - Tu)
Michael Kohlhase, Saarland University, (So - Tu)
Helen Lowe, Glasgow Caledonian University, demo, (Sa - Tu)
Ewen Maclean, University of Edinburgh, talk, (Sa - Tu)
Heiko Mantel, DFKI Saarbruecken, talk, (So - Tu)
Andreas Meier, Saarland University, talk (So - Tu)
Erica Melis, Saarland University, (So - Tu)
Silvio Ranise, University of Genova, talk, (So - Tu)
Axel Schairer, University of Edinburgh, talk, (So - Tu)
Dirk Stefan Schweitzer, TU Darmstadt, talk, (So - Tu)
Joerg Siekmann, DFKI Saarbruecken, (So - Tu)
Werner Stephan, DFKI Saarbruecken, (So - Tu)
Toby Walsh, University of York, (So - Tu)
Christoph Walther, TU Darmstadt, talk, (So - Tu)
Daniele Zini, University of Genova, (So - Tu)

Contact:

Dieter Hutter, DFKI GmbH, Saarbrücken, Germany, hutter@dfki.de Tel. ++49 681 302 5317, Fax. ++49 681 302 2235

9th CLAM - INKA - OMRS Workshop 20.3. - 21.3 2000, Schloss Dagstuhl