##
The Scottish Theorem Proving Seminar

**Room 2A87A **

**Cottrell Building**

**University of Stirling**

*How to get here*
**2-5pm, March 19, 2004**

###
**Programme**

###
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