| 09:00 -- 09:30
|Session 1: Induction and Related Methods
|09:45 -- 10:15
||Lemma Speculation in Higher-order logic
|10:15 -- 10:45
||A Cooperative Approach to Loop Invariant Discovery for Pointer Programs
We propose a cooperative approach to reasoning about the
correctness of pointer programs within the context of
separation logic. A key hurdle to achieving scalable
program proof is the burden imposed by the need for loop
invariants. Pointer data structures can be viewed in
terms of their shape and content. Our
proposal exploits this distinction by combining two
techniques for automating the discovery of loop invariants.
Firstly, a technique developed at CMU for discovering shape
invariants based upon symbolic evaluation. Secondly, middle-out
proof planning, a theorem proving technique applicable
to reasoning about loops and which supports loop invariant discovery.
We believe that the complementary nature of these techniques
will deliver significant advantages in terms of scalable
pointer program proof.
|10:45 -- 11:15
||Improvements in Formula Generalization
For proofs by induction it is often necessary to generalize statements to strengthen the induction hypotheses. We present improved heuristics to generalize away subterms, unnecessary conditions and function symbols in a formula. This resolves shortcomings that we encountered within an experimental evaluation of generalization heuristics from the literature. Our generalization method has been implemented in the verification tool VeriFun. An evaluation with examples from the literature as well as several case studies of our own demonstrates the success of the improvements.
| 11:15 -- 11:30
|Session 2: User Interfaces
|11:30 -- 12:00
||David Aspinall and Christoph Lüth
||Beyond Script Management
|12:00 -- 12:30
||Enabling Proof Assistance Systems to Provide Services in
Texteditors: The Issue of Truth Maintenance
In order to foster the use of proof assistance systems, we integrated
the proof assistant OMEGA into the standard scientific text-editor
TEXMACS. We aim at a document-centric approach to formalising and
verifying mathematics and software, where the author can write her
document without any restrictions while being assisted by OMEGA that
provides its services inside the text-editor. In order to effectively
assist the author, the proof assistance system must be able to maintain
as much of the information about checked parts of the document---for
instance proof steps---through arbitrary modifications of the document.
This requires a sophisticated truth-maintenance system that spans
throughout the whole proof assistance system. We present an enhanced
combination of development graphs and the proof datastructure as a
formal foundation to describe OMEGA's truth maintenance system as well
as the support services offered to the author on that basis.
|12:30 -- 13:00
||Integrating the Text-Editor TeXmacs with the Proof Assistance System OMEGA using
We present a generic mediator, called PLATO, between text editors and proof
assistants and how it served to integrate the proof assistant OMEGA into
TEXMACS. The aim of this mediator is to support the development, formalisation
and publication of mathematical documents as naturally as possible. In
particular PLATO should allow the user to author his mathematical documents
with a scientific WYSIWYG text editor in the informal language he is used to,
that is a mixture of natural language and formulas. These documents can be
semantically annotated preserving the textual structure by using the flexible
parameterised proof language which we present. From this informal semantic
representation PLATO automatically builds up the corresponding formal
representation for a proof assistant, in our case OMEGA. The most important
task of the mediator is the maintenance of consistent formal and informal
representations during the further development of the document in interaction
with OMEGA. The presentation will include a demo of the resulting system.
| 13:00 -- 15:30
|Session 3: Security
|| Graham Steel
||A Formal Theory of Key Conjuring
Key Conjuring is a technqiue used to attack the APIs of tamper proof hardware security modules. We have devised a formal transformtion that takes a set of API rules and determines all the computationally feasible key conjuring operations. This talk will explain what all this means, with plenty of examples.
|| Dietter Hutter
||Preserving Privacy in Web Services Using Information Flow Control
The vision of a landscape of heterogeneous web services
deployed as encapsulated business software assets in the Internet is
currently becoming a reality as part of the Semantic Web. When
pro-active agents handle the context-aware discovery, acquisition,
composition, and management of application services and data,
ensuring the security of customers' data becomes a principle task.
To dynamically compose its offered service, an agent has to process
and spread confidential data to other web services demanding the
required degree of security. In this talk we propose a methodology
based on type-based information flow to control the privacy of
data and their proliferation within a set of communicating web services.
| 16:30 -- 16:45
|Session 4: "Real Mathematics"
|16:45 -- 17:15
||MATHsAiD: an Update
I will present an update on some of the recent developments
with the mathematical theorem discovery system MATHsAiD. In
particular, I will talk about the re-designed hypothesis generator and
the new higher order capabilities of the system. A brief demo will
also be given.
|17:15 -- 17:45
||Ceterum censeo Descente Infinie esse disputandam
We try to give a possible explanation
for the popular erroneous believe that explicit induction is
crucial for the automation of inductive proofs.
We present the only proof of Pierre Fermat by descente infinie
that is known to exist today.
We present a self-contained proof in a modern form,
which nevertheless is intended to follow Fermat's ideas as interpreted
into the cited Latin original.
We then annotate an English translation of Fermat's original
proof with terms from the modern proof.
We offer to discuss descente infinie from the mathematical,
logical, historical, linguistic, and refined logic-historical points of view.
|17:45 -- 18:15
|| Alison Pease
||Lakatos-style reasoning for axiom selection and modification
Lakatos outlined a theory of how mathematical progress may
occur. We consider how this theory may be applied to the selection and
modification of axioms in set theory and geometry.