The Scottish Theorem Proving seminar series
Friday 24th March 2000
Main Lecture Theatre
Institute for System
Level Integration
The Alba Centre
Simpson Parkway
Livingston EH54 7BH
14:00  17:00
Programme
14:00

Welcome


14:10  14:40

Proof Planning for Hardware Verification
Andrew Ireland, HeriotWatt University.


14:50  15:20

Verification Platform for System on Chip
Kong Woei Susanto, University of Glasgow.

15:30  16:00

Refreshments


16:00  16:40

Dependently Typed Records for Representing Mathematical Structure
Randy Pollack, University of Durham and University of Edinburgh.

16:50

Close

17:00 

Checking out Livingston Arms (10min walk away)

Travel to ISLI
Directions on how to reach the Institute are available at
http://www.sliinstitute.ac.uk/About/Wherearewe.html.
Relevant train times are:
Edinburgh Waverley 13:18  Livingston North 13:41,
Glasgow Central 12:15  Livingston South 13:15,
Trains back include:
Livingston North 16:58  Edinburgh Waverley 17:22,
" " 17:28  " " 17:52,
" " 17:58  " " 18:21,
" " 18:28  " " 18:52,
" " 18:58  " " 19:26,
Livingston South 16:52  Glasgow Central 17:59,
" " 18:22  " " 19:29.
If you are travelling to Livingston by train, the ISLI can book and
pay for a taxi to pick you up from one of the train stations: contact
Wendy Glendinning (
Wendy.Glendinning@sliinstitute.ac.uk, 01506469300) before midday
Friday 24th.
The walk from either station is about 35mins, mostly on footpaths away
from roads. It's rather difficult to describe the routes. If you are
keen on sampling these products of new town planning, I could fax you
the relevant section of a map.
Abstracts
Proof Planning for Hardware Verification
Andrew Ireland, HeriotWatt University
Hardware description languages (HDLs), such as Verilog and VHDL,
play a key role in the specification of digital systems. Here we
propose a deductive approach to reasoning about the functional
behaviour of HDL models. Our starting point is modest, we consider
the elementary imperative constructs one would expect to find in any
HDL together with the deductive apparatus required in order to support
temporal reasoning. In terms of deduction we consider a novel extension,
proposed by Mike Gordon, to a FloydHoare style programming logic
that supports temporal reasoning. Following a FloydHoare style of
programming logic means that temporal assertions are embedded within
our HDL models. The effectiveness of this approach to verification relies
upon the adequacy of the specification notation and the power of the
theorem proving technology. It is the theorem proving technology that
is the focus of our proposal. Building upon existing general purpose
theorem proving technology, our aim is to achieve a high degree of
automation within this special purpose verification application. We
see proof planning as providing the basis for achieving this automation.
Verification Platform for System on Chip
Kong Woei Susanto, University of Glasgow
In the near future, the electronics industry will face the reality of
a billion transistors on a chip. With this technology, one can develop
a very large and complex design on a single chip. On the other hand,
the effort to implement a complete system on a chip is enormous and
only a few companies can build the needed competency in all design
areas. These advancements and limitations are forcing traditional
design practices into a new design paradigm of reusable
blocks/components. One approach is for reusable components to be
integrated in an integration platform, which enables the designer to
build a system in a 'plug and play' method. Despite having a
promising future, system integration has major concerns in validation
 how the system as a whole will be verified. The discouraging limits
of traditional validation methods have encouraged the industrial
community to consider formal verification methodologies for checking
hardware system specifications and models. In this talk, I will
present our vision on how we will contribute to solving part of the
problem, in the context of an integration platform approach.
Dependently Typed Records for Representing Mathematical Structure
Randy Pollack, University of Durham and University of Edinburgh
It is folklore that dependently typed tuples suffice to formalize
abstract mathematical structures such as semigroup, monoid, group,
ring, field, ... We want natural properties of informal mathematical
language to be preserved; e.g. inheritance of properties and sharing
of substructures. There is a big literature on the related topic of
programming language modules, and some literature on formalizing
mathematical structure.
In this talk I develop a notion of dependently typed records by adding
field labels to Sigma types. Some obscure features from the
literature are simplified and explained. E.g. field variables (local)
vs field labels (global) are explained by ordinary lambdabinding.
Subtyping is orthogonal to records, and is introduced using Luo's
Coercive subtyping. (Hence I will not explain the subtyping system in
detail, but only show some examples.)
I will discuss the two standard approaches to sharing substructures:
"Pebble style" and "manifest types" (ML style). By example I argue
that we really do need "manifest types" to formalize mathematics, and
extend the dependently typed records to include "manifest types".
Much of my proposed approach can be represented by inductive
definitions in Coq or Lego, so features such as "manifest types" can
easily be experimented with.