The University of Sheffield
Verification and Testing

VT Seminars

The Verification and Testing group holds a weekly research seminar, which usually consists of a talk by an internal or invited external speaker. It also acts as the central time when all members of the group meet, and can thus be used to raise issues and discuss matters. All interested parties are invited to attend.

During the 2008/09 semesters, the seminars were held at 11:00 am on a Monday in G22, unless otherwise specified. The seminars include various other groups like briding-the-gaps and departmental level talks. The varied times will be announced here.

If you would like to give a talk at a future VT seminar, please contact the seminar organiser with an appropriate date. Dates within academic semesters are generally better attended.
Next Seminar: Friday 23 September - 14:10 G30
Speaker: Simon Foster Title: Applying Agda in Model-Driven Design
Agda is a dependently typed functional programming language cum interactive theorem prover. Since proofs are programs, it lends itself ideally for formal program development and construction tasks. However, Agda is still at a very experimental stage and a large amount
of user interaction is needed even for the most basic proof obligations.


Our aim is to probe Agda's potential in formal object-oriented software engineering, deriving model transformations from specifications while proving their correctness. We first present a basic formalisation of object-oriented meta-model specifications in Agda, as well as first steps towards the development of concrete transformations in this setting. We then report on our experimental integration of the automated theorem prover "Waldmeister" into Agda and outline opportunities for future work in this direction. Finally we describe ongoing work intended to enable users to semi-automatically develop formal model transformations that are provably correct, ideally through a form of refinement. We intend to leverage well understood graph transformation and relation algebraic techniques for this task.

2010-2011
Date Title Speaker Slides
23/09/2011 Applying Agda in Model-Driven Design Simon Foster  
08/07/2011 Schema Independent Queryable XML Compression Method OT Dinakenyane  
17/05/2011 An Algebra for Routing Protocols Peter Hoefner (NICTA, Australia) Download
06/05/2011 UI-Driven Test-First Development of Interactive Systems Steve Reeves Download
27/04/2011 Probability and nondeterminism for finite automata Steve Reeves Download
25/03/2011 Integrating an Automated Theorem Prover into Agda Simon Foster and Georg Struth  
17/03/2011
 Testing of biology-inspired systems Prof Florentina Ipate, University of Pitesti  
25/2/2011 Presenting OPTIMIS cloud computing Mariam Kiran  
14/01/2011 Lazy Systematic Unit Testing Tony Simons  

Seminar co-ordinator
The program is organised by Dr. Marian Gheorghe m.gheorghe@dcs.shef.ac.uk