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

CIAO @ 25 - AB @ 70 Workshop

Programme with abstracts

Tuesday 23 May

09:15Dieter Hutter: Reliably secure software systems - six years later
As part of the ending German priority program on Reliably Secure Software Systems a secure conference management system, called CoCon, was developed and verified with respect to its information flow properties. Since the management system is a web-based application running on web-browsers as well as on servers, a variety of different information flow control techniques had to be developed and refined to cope with this scenario. This talk will give an overview on the new techniques in information flow control underlying this case study.
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
Automated theory exploration has the potential to help scientists, mathematicians and programmers discover unexpected properties of their models, theories and programs; but has so far been limited to small-scale experiments, with only a few, hand-picked, data points. We address this problem by re-purposing existing benchmarks from the theorem proving domain, producing an order of magnitude more data for evaluation, and use it to evaluate the performance of a state of the art exploration system. To combat the long run times of these systems, we also propose a pre-processing method to identify promising subsets of a theory, sacrificing completeness to gain speed. It is our hope that the availability of robust evaluation methods, and scalable algorithms, will encourage competition and innovation, making theory exploration more useful and relevant as a formal methods tool.
12:00 Kobby Nuamah: Rich inference frameworks
12:30 LUNCH
13:45 Mateja Jamnik: Accessible reasoning with diagrams
Ontologies are notoriously hard to define, express and reason about. Many tools have been developed to ease the ontology debugging and reasoning, however they often lack accessibility and formalisation. A visual representation language, concept diagrams, was developed for expressing ontologies, which has been empirically proven to be cognitively more accessible to ontology users. In this paper we answer the question of "How can concept diagrams be used to reason about inconsistencies and incoherence of ontologies?". We do so by formalising a set of inference rules for concept diagrams that enables stepwise verification of the inconsistency and incoherence of a set of ontology axioms. The design of inference rules is driven by empirical evidence that concise (merged) diagrams are easier to comprehend for users than a set of lower level diagrams that are a one-to-one translation from OWL ontology axioms. We prove that our inference rules are sound, and exemplify how they can be used to reason about inconsistencies and incoherence.
14:15 Joe Corneli: Reasoning about mathematics with graphical programs
Unlike a classical proof which consists of mathematical statements and deductions, informal mathematical language is more general, and the reasoning involved may be abductive, inductive, or heuristic. This talk will describe a strategy we have been developing for representing mathematical dialogues and other informal texts. A publication appearing in "Artificial Intelligence" this month describes the high-level features of informal mathematics, and helped inspire this project. Our latest efforts produce more detailed models mathematical arguments. A graphical formalism and a corresponding prototype implementation will be described. Applications include modelling collaborative proof dialogues and discursive Q&A, as well as more traditional proofs. In our planned next steps we plan to bring in explicit type-theoretic representations of mathematical objects within a service-oriented architecture.
14:45 Jacques Fleuriot: Mechanizing Euler's infinite (and infinitesimal) reasoning in Isabelle
In his Introductio in Analysin Infinitorum (Introduction to Analysis of the Infinite), Euler made liberal use of infinitesimal and infinite numbers when deriving results such as the series for the exponential and trigonometric functions. However, his approach has been criticised as lacking rigour or even as being reckless. In this talk, we describe how some of the demonstrations from the Introductio, which Euler claimed to need only "ordinary algebra", can be formally reconstructed in the proof assistant Isabelle using concepts and techniques from nonstandard analysis. Along the way, we discuss the appropriateness of our approach and, time permitting, argue that mechanical theorem provers are useful tools for investigating historical mathematics.
15:15 Steven Obua: Interplanetary theorem proving
I recently took a closer look at what the Interplanetary Filesystem is and how it works. It seems to me that it is a natural foundation for some ideas from collaborative theorem proving which were pursued during the ProofPeer project. This talk gives a speculative account of how collaborative theorem proving could be based on the Interplanetary Filesystem.
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
I'll introduce the new EPSRC programme in Human-Like Computing, explain what it is about and how you can get involved. I'll summarise some of the projects I am planning myself.
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
Problem Frames (PF) is a requirements analysis technique that provides a conceptual framework for viewing important groups of problem classes, i.e. patterns for requirements, that aid in the development of good solutions. It also introduces the notion of concerns that help shed light on potential faults that should to be considered early in design. However, PF notations are not familiar or accessible to industry practitioners with respect to languages like UML/SysML. We extend SysML to inherit the characterisation of structure from PF which subsequently supports the application of problem classes--we call these behavioural interaction patterns--on the behaviour model elements. This provides: (1) a systematic means of fitting requirements to structure and behaviour represented in SysML; and (2) the use of concerns to identify and record patterns for accident and recovery.
11:45 Gudmund Grov: Tactics for the Dafny program verifier
12:30-13:30 LUNCH
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.