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

CIAO @ 25 - AB @ 70 Workshop
Edinburgh, Scotland

Tuesday 23 - Wednesday 24 May 2017


This year it is the 25th anniversary of the start of what has become the CIAO workshop series which covers topics relating to the automation of mathematical reasoning, such as proof planning, verification, theory exploration and ontology evolution. This year is also the year of Alan Bundy's 70th birthday.

This workshop is to celebrate both these anniversaries. It will consist of talk sessions and one or two panel sessions, with plenty of time to mix with other workshop participants.

Organiser: Paul Jackson.

Important Dates


Deadline for Registration: Friday 5th May 2017


There is no registration fee. Refreshments and lunches both days and dinner the first day will all be provided.

If you plan to attend, please send an email to Paul Jackson (Paul.Jackson at Please let me know the following:


The workshop will be held in Room 2.33 of the Informatics Forum on the central campus of the University of Edinburgh.

The evening buffet meal on Tuesday will be held in the Raeburn Room in the nearby Old College building of the University.


A programme with abstracts for most talks is also available.

Tuesday 23 May

09:15Dieter Hutter: Reliably secure software systems - six years later
10:00David Aspinall: Formal methods, machine learning and mobile security
11:00 Andriana Gkaniatskou: Low-level analysis of cryptographic protocols
11:30 Chris Warburton: Quantitative benchmarks for theory exploration
12:00 Kobby Nuamah: Rich inference frameworks
12:30 LUNCH
13:45 Mateja Jamnik: Accessible reasoning with diagrams
14:15 Joe Corneli: Reasoning about mathematics with graphical programs
14:45 Jacques Fleuriot: Mechanizing Euler's infinite (and infinitesimal) reasoning in Isabelle
15:15 Steven Obua: Interplanetary theorem proving
15:45 BREAK
16:15-17:45 PANEL: Automated reasoning support for mathematics: past expectations, future challenges.

There has long been a hope that automated reasoning could be useful in mathematics education or mathematics research. In 1994/5 the QED Manifesto and QED meetings explored this theme. This summer the Newton Institute is hosting the Big Proof programme. How has progress in the recent decades been different from past expectations. Why? What big challenges remain to be addressed? Where might we be in the next decade or two?
18:30-21:00 BUFFET DINNER

Wednesday 24 May

09:00 Fausto Giunchiglia: Computational humanism
09:45 Alan Bundy: Human-like computing
10:15 BREAK
10:45 Petros Papapanagiotou: WorkflowFM: a logic-based framework for formal process specification and composition
11:15 Rajiv Murali: UsecasePro: a rigorous approach to Use Case Driven Development in SysML
11:45 Gudmund Grov: Tactics for the Dafny program verifier
12:30-13:30 LUNCH


For hotels and guest houses near the Informatics Forum, view this map. Clicking on the hotel or guest house name on the left will show its location on the map and provide a link to its website.

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.