Scottish Theorem Proving Meeting @ University of Glasgow

On Tuesday June 6th 2006, a Scottish Theorem Proving meeting will take place at the University of Glasgow. The meeting will be hosted by the Department of Computing Science and will take place in Room F121 (conference room), on the 1st floor of the Computing Science building, 17 Lilybank Gardens, G12 8QQ. The Computing Science building is marked as D16 on the campus map. If you wish advice on how to reach the University of Glasgow by train, taxi, bus, car, bike, etc., have a look at the Maps and Travel page. For all organisational issues, please contact Alastair Donaldson (


1.00pm - 2.00pm: Lunch

A sandwich lunch will be provided in the departmental common room. Please contact Alastair Donaldson as soon as possible, and before June 4th, if you would like to come for lunch, so that appropriate catering arrangements can be made.

2.10pm - 2.45pm: Towards a Verification Tool for Quantum Communication Protocols

Nick Papanikolaou (joint work with Rajagopal Nagarajan and Simon Gay)
FMW Group

Department of Computer Science, University of Warwick


In this talk we will discuss work in progress with Rajagopal Nagarajan (Warwick) and Simon Gay (Glasgow) on developing a verification tool based on model-checking for analysing communication and cryptographic protocols involving quantum mechanical phenomena. We will give an account of earlier work, including the quantum process algebra CQP, and the verification of BB84 and other protocols using the PRISM model checker. In particular, we will explain the PRISMGEN tool developed in Glasgow and our early successes with this; an emphasis will be put on the use of concepts from group theory, and how the so-called stabilizer formalism may help in representing quantum protocols efficiently. This work is partially supported by EPSRC (GR/S34090/01). My visit has been made possible through the generous support of SymNet.

2.45pm - 3.20pm: The New Proof Assistant OMEGA: Developments and Applications

Serge Autexier
German Research Center for Artificial Intelligence and Centre for Intelligent Systems and their Applications, University of Edinburgh


I will give an overview of the new version of the proof assistant system OMEGA. The talk will be a walkthrough of the new parts of the system, starting from the maintenance of structured theories, the infrastructure for deep-inferential, assertion-level proof planning and proof construction, the integration of OMEGA into a scientific text-editor TEXMACS. I will conclude the talk by discussing ongoing/future developments for automation of proof search, including a short overview of the goals of the EPSRC Visiting Researcher project I'm currently on visiting the DREAM group.

3.20pm - 3.50pm: Tea and Coffee

3.50pm - 4.25pm: Performance and Dependability Analysis of Fault-tolerant Memory Mechanisms using Stochastic Well-formed Nets

Paolo Ballarini
FATA Group

Department of Computing Science, University of Glasgow


Memory fault-tolerance for a computer system can be achieved through a combination of hardware replication and appropriate software access mechanisms based on majority voting. In this work we show how dependability and performance of such a fault-tolerant framework can be assessed by means of a combination of combinatorial techniques and state-space analysis of specific Petri Nets models. This work is part of a EU funded project named TIRAN: TaIlorable fault toleRANce framework for embedded applications.

4.25pm - 5.00pm: Towards Automatic Assertion Refinement for Separation Logic

Andrew Ireland
Dependable Systems Group

School of Mathematical and Computer Sciences, Heriot-Watt University


Separation logic holds the promise of supporting scalable formal reasoning for pointer programs. Here we consider proof automation for separation logic. In particular we propose an approach to automating partial correctness proofs for recursive procedures. Our proposal is based upon proof planning and proof patching via assertion refinement.

5pm: Retire to the Brel bar, Ashton Lane, G12 8SJ, for drinks.