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 MiniPolymath projects 20092012) 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; metalevel 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 dataled rather than philosophyled 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 EventB 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 EventB models. However, as well as generating code, our approach also automatically generates code level specifications, i.e. SPARK pre and postconditions, along with loop invariants. In terms of the SPARK proof tools, having the loop invariants increases verification automation. A prototype, known as ESPARK, has been implemented as a plugin for the Rodin Platform (EventB toolkit), and tested on a range of examples, i.e. searching, sorting and numeric calculations.  
15.00  Yu Lu  Model Checking PortBased 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 portbased 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 EventB Invariant Preservation Proofs 
In this talk I will present the use of rippling in EventB
invariant proofs. I will show that rippling is applicable for EventB
invariant preservation proof obligation. Then I will talk about the
use of schemebased 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