09:00  WELCOME 

09:15  Dieter 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 webbased
application running on webbrowsers 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:00  David Aspinall: Formal methods, machine learning and mobile security 



10:30  BREAK 

11:00  Andriana Gkaniatskou: Lowlevel 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
smallscale experiments, with only a few, handpicked, data points. We
address this problem by repurposing 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 preprocessing 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 onetoone 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 highlevel 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 typetheoretic representations of mathematical objects within a
serviceoriented 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:1517: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:3021:00  BUFFET DINNER 