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.
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 ed.ac.uk). Please let me know the following:
Talks are welcome on any topics you are excited about and you think would be of interest to other participants. High-level talks surveying recent accomplishments, expressing visions of the future and exploring challenges ahead are particularly encouraged.
Talks will be scheduled in half hour time slots, but some talks could have longer, if appropriate.
The evening buffet meal on Tuesday will be held in the Raeburn Room in the nearby Old College building of the University.
|09:15||Dieter Hutter: Reliably secure software systems - six years later|
|10:00||David 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|
|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|
|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?
|09:00||Fausto Giunchiglia: Computational humanism|
|09:45||Alan Bundy: Human-like computing|
|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|