The Scottish Theorem Proving seminar series

9th May 1997
Department of Computing Science
University of Glasgow

14:00 - 17:00

F171
Department of Computing Science
University of Glasgow
17 Lilybank Gardens
Glasgow.

How to get here

Some information on how to get here is given on the departmental pages. It is worth noting that it is difficult to find parking spaces around the university.

Instructions for getting here from Rail Station:

Get into the underground and go around to Hillhead Station. The department is just up the hill "behind" the station:

      ---------- Byres Road -----U------------+-------------
                             (Hillhead)       |
                                              |
                                              | (Great George Street)
                                              |
                                              |
             /--------------------------------+
             |                                |
              \-------------------------------+ <<--- Lilybank Gardens
                 [][][][][] Houses [][][][][] |
                 /\                           |
         CS Dept in House 17
         Walk up Lilybank Gardens
         and enter from the front door

Otherwise:

Get into a taxi, and ask the to take you to 17 Lilybank Gardens, just off Great George Street.

Eating out

There are many places to eat near the department. If you arrive early and want to meet others for lunch then we suggest the Metro. It is self service so it doesn't matter if people arrive at different times. There is a variety of food and plenty of space. How to get there:
From Hillhead underground
Turn right at the exit and walk along Byres Road. Then turn first right onto Great George St. Then first left into the lane. The Metro is on the left (big glass doors).

From the department
Turn right at the exit and walk along lilybank Gardens. Then turn left onto Great George St. Then first right into the lane. The Metro is on the left (big glass doors).

Programme

14:00Start & Welcome
14:10 - 14:40 The Logic of Search Procedures
Judith Underwood, University of Glasgow.
14:50 - 15:20 Reasoning about an Embedding of a Hardware Description Language in Haskell
Graham Collins and Jonathan Hogg, University of Glasgow
15:30Coffee
16:00 - 16:45 Reasoning about VDM specifications with PVS
Savi Maharaj, University of Stirling
17:00Finish
Times in red are fixed.
Times in blue are flexible.

Abstracts

Reasoning about VDM specifications with PVS
Savi Maharaj, University of Stirling

The PVS system is a formal specification tool developed at SRI in California. It has a very expressive specification language consisting of classical higher-order logic enhanced with many useful features such as subtyping, dependent types, theories, overloading, and recursive definitions. This is combined with a interactive theorem prover in which powerful tactics and decision procedures are tightly integrated with more basic proof commands.

I'm going to talk about applying PVS to specifications written in the style of VDM (invariants, pre- and postconditions, refinements from abstract to concrete, etc). Because the PVS language is so expressive, it is straightforward to express VDM-style specifications within it by means of a "shallow embedding". There is a paper by Sten Agerholm which describes how this can be done. The embedding does not reflect VDM accurately because the logics of VDM and PVS are not the same; it is also difficult to extend the embedding to incorporate more of VDM because PVS is not implemented as an "open" system. For these reasons, Agerholm's conclusions are essentially negative. My view is somewhat more optimistic: I think that adopting VDM style provides a useful methodology for exploiting the power of PVS.

The Logic of Search Procedures
Judith Underwood, University of Glasgow.
(joint work with Ian Gent, University of Strathclyde)

Efficient search procedures for NP-complete problems are of intense practical interest, and many improvements on standard backtracking search have been proposed. However, these improvements are often described only for a particular kind of problem (e.g. binary constraint satisfaction) and the pruning techniques are seldom proved sound when they are introduced. In this talk, I will describe a general framework for the development of a search procedure as the computational content of a proof, and show how this technique can be used to prove the correctness of sophisticated search strategies. This approach separates the search algorithm from problem-specific data manipulation routines, enabling rapid implementation for new problem classes.

Reasoning about an Embedding of a Hardware Description Language in Haskell
Graham Collins and Jonathan Hogg, University of Glasgow

We describe some experiments with using a theorem prover to investigate a translation of a relational hardware description language into a functional language in such a way that the user does not have to decide the direction of the data flow in the functional language. This approach relies on laziness, making the translation both hard to reason about and unsuitable for easy embedding in most theorem provers.
Return to Scottish Theorem Proving page.