CIAO 2005 Programme

Monday 4th April

Session 1, B53: Verifying Programs and Protocols Chair: Louise Dennis
1pm	On Reasoning About Pointer Based Programs Andrew Ireland
1.40pm	Automated Reasoning by Supercompilation Alexei Lisitsa and Andrei Nemytykh
2.20pm	XOR Constraints in Security API Modelling Graham Steel
3pm	Coffee
Session 2, B53: Induction I Chair: Jürgen Zimmer
3.30pm	Using Induction for Cut-Simulation Chad Brown
4.10pm	Constructing Induction Rules for Deductive Synthesis Proofs - Alan Bundy
7.30pm Dinner, Mem Saab, 12-14 Maid Marian Way, Nottingham

Tuesday 5th April

Session 3, B53: Proof Presentation and Mathematical Notation Chair: Roy McCasland
9.30am	Intuitive and Formal Representations: The Case of Matrices Manfred Kerber, Martin Pollet and Volker Sorge
10.10am	Proof Presentation Jörg Siekmann
10.50am	Coffee
Session 4, B53: Proof Presentation II Chair: Lucas Dixon
11.30am	Novel Directions in the OMEGA Project Christoph Benzmüller
12.10pm	Formalising and Analysing Textbook Proofs: The Problem of Under-Specification and Granularity Serge Autexier
12.50pm	Lunch
Session 5, B53: Induction II Chair: Gudmund Grov
2pm	Experiences proving the Correctness of Student Functional Programs in Isabelle Louise Dennis and Pablo Nogueria-Iglesias
2.40pm	Rippling Rippling Lucas Dixon
3.20pm	Coffee
3.50pm	CIAO Business Meeting, B53 Chair: Alan Bundy

Wednesday 6th April

Session 6, B53: Integration of Reasoning Systems Chair: Fiona McNeill
9.30am	Can a Higher-Order and a First-Order Theorem Prover Cooperate? Volker Sorge and Christoph Benzmüller
10.10am	The verification of programs in Hume Gudmund Grov
10.50am	Coffee
Session 7, B53: e-Science and Grid Applications Chair: Manfred Kerber
11.30am	Intelligent Brokering of Semantic Reasoning Web Services Jürgen Zimmer
12.10pm	Dynamic Ontology Refinement Fiona McNeill
12.50pm	Towards a bell-curve calculus and its application to e-Science Lin Yang
1.40pm	Close