|
|
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 (ally@dcs.gla.ac.uk).
Abstract
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.
Abstract
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.
Abstract
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.
Abstract
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.