The Scottish Theorem Proving Seminar

Room 2A87A  
Cottrell Building
University of Stirling
How to get here

2-5pm, March 19, 2004


Programme

2:00 A Methodology for Theory Development: VDM Proof Obligations via Proof Planning
Helen Lowe
2:45 Investigating structural symmetry in models of concurrent systems
Alastair Donaldson
3:30 Coffee break
4:15 Higher Order Rippling in IsaPlanner
Lucas Dixon
5:00 Close


A Methodology for Theory Development: VDM Proof Obligations via Proof Planning

Helen Lowe
University of Strathclyde

Although a wide variety of powerful theorem provers have emerged from the academic theorem proving community, and an increasing interest in proof in the software development community, take up of prover technology has been disappointing. One idea is that proof tools need to be introduced as a ``Trojan Horse'' into existing CASE tools in order to be accepted. A barrier to this could be the need to understand failing proofs in order for a proof tool to be at all useful. We examine a subset of interesting problems from the point of view of potential end-users, and describe a methodology using existing theorem provers which could be harnessed to solve such problems.


Investigating structural symmetry in models of concurrent systems

Alastair Donaldson
University of Glasgow

Over the last decade, symmetry reduction techniques have been shown to be successful in combating the state space explosion problem in model checking. Such reduction techniques usually assume that symmetries of a concurrent system are known in advance, and these symmetries are exploited when model checking the original system description. Two obvious questions are a) "can we automatically detect symmetries of a concurrent system from its textual description?", and b) "would it be possible to apply symmetry reduction directly to the textual description of a system so that a reduced textual description could be model checked in the usual way?". In my talk I will describe some preliminary work in attempting to answer these questions.


Higher Order Rippling in IsaPlanner

Lucas Dixon
University of Edinburgh

We present an account of rippling with proof critics suitable for use in higher order logic in Isabelle/IsaPlanner. We treat issues not previously examined, in particular regarding the existence of multiple annotations during rippling. This results in an efficient mechanism for rippling that can conjecture and prove needed lemmas automatically, and then present the resulting proof plans as Isar style proof scripts.



For further information contact Savi Maharaj

STPS homepage