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, Heriot-Watt 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.sli-institute.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@sli-institute.ac.uk, 01506-469300) before mid-day 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, Heriot-Watt 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 Floyd-Hoare style programming logic that supports temporal reasoning. Following a Floyd-Hoare 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 semi-group, 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 lambda-binding. 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.

Return to Scottish Theorem Proving page.