MRG home page Research Publications Projects Software People

Scottish Theorem Provers Meeting
@ The University of Edinburgh

14 December 2012

Organiser: Alan Smaill

Location

Informatics Forum
Room G.03
Crichton Street
Edinburgh, EH8 9AB

Our location

Programme

13.30 Tea, coffee outside G.03
14.00 Andrew Aberdein

Alison Pease

An Empirical Investigation into Explanation in Mathematical Conversations


Analysis of online mathematics forums can help reveal how explanation is used by mathematicians. We searched four discussions (Gowers and Tao's Mini-Polymath projects 2009-2012) for question indicators, premise indicators, and conclusion indicators. We thereby developed typologies of questions and explanations. One type of questions ask for an object, mathematical or otherwise, such as an example, a classification, categorisation, argument, technique, justification, conjecture, or explanation. We found explanations about flaws in reasoning; meta-level reasoning about proof strategies; reasons why the truth of a mathematical statement cannot be known; and clarifications. We investigated the structure of these explanations and the understanding shown by other participants before and after an explanation. Novelties of our approach include an emphasis on mathematics in progress rather than as finished product, a data-led rather than philosophy-led approach, and a focus on the collaborative work characteristic of much mathematical research.
14.30 Rajiv Murali Automated Generation of Provably Correct Code from Formally Verified Designs


An approach to generating provably correct sequential code from formally developed algorithmic designs is presented. Given an algorithm modelled in the Event-B formalism, we automatically translate the design into the SPARK programming language. Our translation builds upon Abrial's approach to the development of sequential programs from Event-B models. However, as well as generating code, our approach also automatically generates code level specifications, i.e. SPARK pre- and post-conditions, along with loop invariants. In terms of the SPARK proof tools, having the loop invariants increases verification automation. A prototype, known as E-SPARK, has been implemented as a plugin for the Rodin Platform (Event-B toolkit), and tested on a range of examples, i.e. searching, sorting and numeric calculations.
15.00 Yu Lu Model Checking Port-Based Network Access Control for Wireless Networks
We could use model checking to help analyse security protocols by exhaustively inspecting reachable composite system states in a finite state machine representation of the system. The IEEE 802.1X standard provides port-based network access control for hybrid networking technologies. We describe how the current IEEE 802.1X mechanism for 802.11 wireless networks can be modelled in PROMELA modelling language and verified using SPIN model checker. We aim to verify a set of essential security properties of the 802.1X, and also to find out that whether the current combination of the IEEE 802.1X and 802.11 standards provide a sufficient level of security.
15.30 Tea, coffee outside G.03
16.00 Yuhui Lin The Use of Rippling to Automate Event-B Invariant Preservation Proofs

In this talk I will present the use of rippling in Event-B invariant proofs. I will show that rippling is applicable for Event-B invariant preservation proof obligation. Then I will talk about the use of scheme-based theorem lemma conjecturing when rippling is blocked due to the missing lemmas.
16.30 Conor McBride A polynomial testing principle

Two polynomial functions of degree at most n agree on all inputs if they agree on n + 1 different inputs, e.g., on {0, 1, 2, ... , n}. This fact gives us a simple procedure for testing equivalence in a language of polynomial expressions. Moreover, we may readily extend this language to include a summation operator and test standard results which are usually established inductively. I present a short proof of this testing principle which rests on the construction and correctness of a syntactic forward- difference operator.
17.00 Retire to some nearby venue

Previous STP seminars
For further information please contact: level2admin via inf.ed.ac.uk