| 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