The Scottish Theorem Proving seminar series
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:00 | Start & 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:30 | Coffee |
| 16:00 - 16:45 |
Reasoning about VDM specifications with PVS
Savi Maharaj, University of Stirling |
17:00 | Finish |
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.