MRG home page · Research · Publications · Projects · Software · People

CIAO 2007 Workshop



The 16th CIAO workshop will be on the 4rd and 5th of April 2007, hosted at The Burn near Brechin, organised by the Mathematical Reasoning Group, University of Edinburgh

Foreword

The CIAO workshop is intended to provide a snapshot of research into automating mathematical reasoning, especially in the areas of proof planning, rippling, verification and related areas. The CIAO-2007 workshop is inviting participation from groups involved in closely related research.

Organisers: Natalia Deringer, Lucas Dixon, Fiona McNeill, Graham Steel


Important Dates | Programme | Travel Information | Registration


See photos from CIAO-2007
and more more photos from CIAO-2007, thanks to Deiter

Important Dates

Workshop Dates: 4rd-5th April 2007

Deadline for Registration: 28th February 2007

Registration

If you plan to attend the CIAO Workshop, please send an email to Lucas Dixon by the 28th of February. Please let us know about the following:

Location

The Burn
Glenesk
Brechin
Angus DD9 7YP

Google Map

Travel Information

You can get to the Burn by taking a train to Montrose and then a bus to Edzell (in Angus) and finally walking, cycling, or taking a taxi for the last 1 and a half miles. We can also pick people up from Montrose train station - if you would like a lift please let us know. If you take the bus, ask to be dropped off at the driveway to the Burn which will then leave you with only a short walk.

Food will be provided with the accommodation, including a meal at 7pm on the 3rd of April.

We will organise a minibus leaving from Edinburgh on the afternoon of the 3rd of April, leaving at 12:20pm from the front of Appleton Tower. Roy McCasland and Paul Jackson will also be driving and giving people lifts. The transport plan has been added to the participants table below.

More Travel links:

Accommodation

The Burn has 20 bedrooms. Accommodation (including food) will be 60 pounds per person per night. Students get a discounted rate of 38 pounds, although a towel is not provided with the discounted rate - so either bring your own or buy one in Edinburgh before hand. There is a licensed bar that will be open until 10pm. If you have any dietary requirements, please let us know in the registration email. In order to pay for accommodation we have managed to get our finance department to take credit/debit card payments online (via worldpay). What you need to do in order to pay for accommodation is:

Please pay by the 10th of March!

Food will be provided with the accommodation, including a meal at 7pm on the 3rd of April. Note that for the student price, the burn do not provide a towel, so you may want to bring one, or buy one in Edinburgh before we leave.

Equipment and Computing Facilities

The Seminar Room contains a whiteboard, OHP and Data Projector.

Participants (22)

Name Transport Room
Markus Aderhold (Darmstadt) By car with Roy, meeting at the Aiport at 13:15. Room 14
Christoph Walther (Darmstadt) By car with Roy, meeting at the Aiport at 13:15. Room 11
Dieter Hutter (DFKI) Hired car with Family Rooms 5 and 6
Dominik Dietrich (Saarbrücken) Minibus, meeting at Appleton Tower 12:20 Rooms 17
Marc Wagner (Saarbrücken) Minibus, meeting at Appleton Tower 12:20 Room 17
Serge Autexier (Saarbrücken) Minibus, meeting at Appleton Tower 12:20 Room 3
Andreas Franke (Saarbrücken) Minibus, meeting at Appleton Tower 12:20 Room 9
Lilia Georgieva (Heriot-Watt) By car with Paul Jackson Room 15
Andrew Ireland (Heriot-Watt) By car with Paul Jackson Room 2
Ianthe Hind (Heriot-Watt) Minibus, meeting at Appleton Tower 12:20 Room 7
Alan Bundy (University of Edinburgh) By car with Paul Jackson James Russell suite
Alan Smaill (University of Edinburgh) By car with Roy Room 10
Roy McCasland (University of Edinburgh) By car with others Room 16
Moa Johansson (University of Edinburgh) Minibus, meeting at Appleton Tower 12:20 Room 7
Graham Steel (University of Edinburgh) Minibus, meeting at Appleton Tower 12:20 Room 4
Fiona McNeill (University of Edinburgh) Minibus, meeting at Appleton Tower 12:20 Room 13
Lucas Dixon (University of Edinburgh) Minibus, meeting at Appleton Tower 12:20 Room 4
Alison Pease (University of Edinburgh) Minibus, meeting at Appleton Tower 12:20 Room 13
Paul Jackson (University of Edinburgh) By car with others Room 16
David Aspinall (University of Edinburgh) Minibus, meeting at Appleton Tower 12:20 Room 1
Christoph Lüth (University of Edinburgh/DFKI) Minibus, meeting at Appleton Tower 12:20 Room 1
Claus Peter Wirth (Technische Universität Wien) Minibus, meeting at Appleton Tower 12:20 Room 8

Programme

Talks should be 20 Minutes with 10 minutes for questions. Note the long lunch break - this is to give participants time to explore the countryside around The Burn..

Day 1: Wed 4th April

09:00 -- 09:30 Breakfast
Session 1: Induction and Related Methods
09:45 -- 10:15 Moa Johansson Lemma Speculation in Higher-order logic
10:15 -- 10:45 Andrew Ireland A Cooperative Approach to Loop Invariant Discovery for Pointer Programs
We propose a cooperative approach to reasoning about the correctness of pointer programs within the context of separation logic. A key hurdle to achieving scalable program proof is the burden imposed by the need for loop invariants. Pointer data structures can be viewed in terms of their shape and content. Our proposal exploits this distinction by combining two techniques for automating the discovery of loop invariants. Firstly, a technique developed at CMU for discovering shape invariants based upon symbolic evaluation. Secondly, middle-out proof planning, a theorem proving technique applicable to reasoning about loops and which supports loop invariant discovery. We believe that the complementary nature of these techniques will deliver significant advantages in terms of scalable pointer program proof.
10:45 -- 11:15 Markus Aderhold Improvements in Formula Generalization
For proofs by induction it is often necessary to generalize statements to strengthen the induction hypotheses. We present improved heuristics to generalize away subterms, unnecessary conditions and function symbols in a formula. This resolves shortcomings that we encountered within an experimental evaluation of generalization heuristics from the literature. Our generalization method has been implemented in the verification tool VeriFun. An evaluation with examples from the literature as well as several case studies of our own demonstrates the success of the improvements.
11:15 -- 11:30 Coffee
Session 2: User Interfaces
11:30 -- 12:00 David Aspinall and Christoph Lüth Beyond Script Management
12:00 -- 12:30 Serge Autexier Enabling Proof Assistance Systems to Provide Services in Texteditors: The Issue of Truth Maintenance
In order to foster the use of proof assistance systems, we integrated the proof assistant OMEGA into the standard scientific text-editor TEXMACS. We aim at a document-centric approach to formalising and verifying mathematics and software, where the author can write her document without any restrictions while being assisted by OMEGA that provides its services inside the text-editor. In order to effectively assist the author, the proof assistance system must be able to maintain as much of the information about checked parts of the document---for instance proof steps---through arbitrary modifications of the document. This requires a sophisticated truth-maintenance system that spans throughout the whole proof assistance system. We present an enhanced combination of development graphs and the proof datastructure as a formal foundation to describe OMEGA's truth maintenance system as well as the support services offered to the author on that basis.
12:30 -- 13:00 Marc Wagner Integrating the Text-Editor TeXmacs with the Proof Assistance System OMEGA using PLATO
We present a generic mediator, called PLATO, between text editors and proof assistants and how it served to integrate the proof assistant OMEGA into TEXMACS. The aim of this mediator is to support the development, formalisation and publication of mathematical documents as naturally as possible. In particular PLATO should allow the user to author his mathematical documents with a scientific WYSIWYG text editor in the informal language he is used to, that is a mixture of natural language and formulas. These documents can be semantically annotated preserving the textual structure by using the flexible parameterised proof language which we present. From this informal semantic representation PLATO automatically builds up the corresponding formal representation for a proof assistant, in our case OMEGA. The most important task of the mediator is the maintenance of consistent formal and informal representations during the further development of the document in interaction with OMEGA. The presentation will include a demo of the resulting system.
13:00 -- 15:30 Lunch
Session 3: Security
15:30--16:00 Graham Steel A Formal Theory of Key Conjuring
Key Conjuring is a technqiue used to attack the APIs of tamper proof hardware security modules. We have devised a formal transformtion that takes a set of API rules and determines all the computationally feasible key conjuring operations. This talk will explain what all this means, with plenty of examples.
16:00--16:30 Dietter Hutter Preserving Privacy in Web Services Using Information Flow Control
The vision of a landscape of heterogeneous web services deployed as encapsulated business software assets in the Internet is currently becoming a reality as part of the Semantic Web. When pro-active agents handle the context-aware discovery, acquisition, composition, and management of application services and data, ensuring the security of customers' data becomes a principle task. To dynamically compose its offered service, an agent has to process and spread confidential data to other web services demanding the required degree of security. In this talk we propose a methodology based on type-based information flow to control the privacy of data and their proliferation within a set of communicating web services.
16:30 -- 16:45 Coffee
Session 4: "Real Mathematics"
16:45 -- 17:15 Roy McCasland MATHsAiD: an Update
I will present an update on some of the recent developments with the mathematical theorem discovery system MATHsAiD. In particular, I will talk about the re-designed hypothesis generator and the new higher order capabilities of the system. A brief demo will also be given.
17:15 -- 17:45 CP Wirth Ceterum censeo Descente Infinie esse disputandam
We try to give a possible explanation for the popular erroneous believe that explicit induction is crucial for the automation of inductive proofs. We present the only proof of Pierre Fermat by descente infinie that is known to exist today. We present a self-contained proof in a modern form, which nevertheless is intended to follow Fermat's ideas as interpreted into the cited Latin original. We then annotate an English translation of Fermat's original proof with terms from the modern proof. We offer to discuss descente infinie from the mathematical, logical, historical, linguistic, and refined logic-historical points of view.
17:45 -- 18:15 Alison Pease Lakatos-style reasoning for axiom selection and modification
Lakatos outlined a theory of how mathematical progress may occur. We consider how this theory may be applied to the selection and modification of axioms in set theory and geometry.
18:30 Bar opens
19:00 Dinner
22:00 Bar closes

Day 2: Thu 5th April

09:00 -- 09:30 Breakfast
Session 5: Representation and Reasoning
09:45--10:15 Dominik Dietrich What comes above the Assertion Level?
I give an overview about the current state of the omega prover. Starting from inferences, which are the atomic proof building blocks in omega and work directly at the assertion level, we will reach the concept of a strategy, which is the main concept for performing search. Finally I present ideas of how to organize search at the strategy level which I want to discuss with you during the week in Scotland.
10:15 -- 10:45 Fiona McNeill Structural Semantic Matching
10:45 -- 11:15 Alan Bundy Towards a Theory of Ontology Repair or Truthfulness Considered Harmful
We give a formal definition of the problem of ontology repair and are working towards formal definitions of some ontology repair operations. We note that truthfulness in an ontology repair operation is an undesirable property as it makes it difficult, if not impossible, then to use it for ontology repair. To avoid truthfulness, and related problems of inconsistency and definitional vagueness, in the straightforward syntactic definitions of these repair operations, we are experimenting with semantic alternatives. We plan to prove theoretic properties of these semantically defined repair operations and to implement them and evaluate them experimentally.
11:15 -- 11:30 Coffee
Session 6: Theory
11:30 -- 12:00 Alan Smaill Procedural proofs and reflection principles
Several people locally in Edinburgh have made use of inference systems loosely inspired by the constructive omega rule for the natural numbers, which allows a universally quantified statement to be inferred from a suitable effective procedure that generates the proofs of the individual instances. Torkel Franzen suggested that the formalisations used could more accurately be regarded as making use of a proof-theoretic reflection principle over a standard initial logic. I will explain what is involved, and why I think this suggestion is right.
12:00 -- 12:30 Paul Jackson Formal Languages for Mathematics
Most formalised mathematics is hard to read. This talk looks at how to bring the formal language of terms, types and formulas closer to that used in textbooks and papers. After reviewing awkwardnesses of the HOL language, the talk explores richer languages based on more expressive type systems and set theory foundations (e.g. that of the Mizar proof assistant) and makes suggestions for future research in this area.
12:30 -- 13:00 Lucas Dixon Datatype Morphisms
We consider a deep embedding of a restricted class of datatypes (and-or trees) in order to implement some useful morphisms. As an example, we consider the automatic creation of the zipper. This gives two directions for such morphisms: as machinery to support generic programming, and as another class of theory formation.
13:00 -- 14:30 Lunch & CIAO Business Chat

Previous CIAO Workshops

Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.