The Scottish Theorem Proving seminar series

Friday 11th June 1999

Lecture Theatre A1,
Cottrell Building,
University of Stirling

14:00 - 16:45

Speakers

1400 - 1440 "A Quick SPIN around Model-Checking"
Muffy Calder,
University of Glasgow
1440 - 1500 "Test Case Extraction from Correctness Proofs"
Savi Maharaj
University of Stirling
1500 - 1530 tea
1530 - 1550 "VSDITLU: a verifiable symbolic definite integral table look-up"
Dr Andrew A Adams
University of St Andrews
1550 - 1630 "A Semantic Connection between STE and HOL"
Tom Melham,
University of Glasgow

Abstracts

"A Quick SPIN around Model-Checking"

SPIN is a model-checker from Bell Labs which (through its associated language Promela) supports on-the-fly checking of concurrent systems with both synchronous and asynchronous communication, dynamic allocation of processes, and channels as messages. So, it is particularly well suited to application domains where these aspects are important (e.g. telecommunications, protocols, etc.)

Checking is both with respect to in-line assertions, or process invariants, as well as those expressible in a temporal logic. In this quick tour, I will illustrate some of the features of the language and the reasoning capabilities, as well as some of the more interesting "challenges" we have encountered at Glasgow when using both in earnest.

"Test Case Extraction from Correctness Proofs"

Testing is an essential but expensive part of the software development process. There is a need for methods and tools which produce test data which are carefully chosen so as to maximize the proportion of program bugs which are discovered without greatly increasing the volume of tests which need to be carried out.

The approach which I explore is inspired by work on the extraction of test cases from algebraic or model-based specifications of programs. I propose to extend this approach by taking also a high-level or relatively abstract implementation of a specified program, as well as a formal proof of the program's correctness. Carrying out a correctness proof often entails detailed analysis of the input domain of a program, partitioning that domain into subdomains for which a uniform argument is used to establish correctness.

My hypothesis is that this partitioning is a useful and meaningful artefact of the proof process and can be used as the basis for extracting test cases which can then be used for validating further, less abstract, implementations of the specification. These test cases will be more effective at fault detection than test cases selected by other methods because of the semantically meaningful way in which they have been chosen.

The talk describes some preliminary experiments which we conducted using a small example.

"VSDITLU: a verifiable symbolic definite integral table look-up"

We present a verifiable symbolic definite integral table look-up: a system which matches a query, comprising a definite integral with parameters and side conditions, against an entry in a verifiable table and uses a call to a library of facts about the reals in the theorem prover PVS to aid in the transformation of the table entry into an answer. Our system is able to obtain correct answers in cases where standard techniques implemented in computer algebra systems fail. We present the full model of such a system as well as a description of our prototype implementation showing the efficacy of such a system: for example, the prototype is able to obtain correct answers in cases where computer algebra systems [CAS] do not. We extend upon Fateman's web-based table by including parametric limits of integration and queries with side conditions.
(Joint work with Gottliebsen, Linton and Martin.)

"A Semantic Connection between STE and HOL"

In this talk, I will describe some recent work on establishing a semantic connection between the Symbolic Trajectory Evaluation model-checking algorithm and relational verification in higher-order logic. The main result is a theorem that translates correctness results from trajectory evaluation over a four-valued lattice into a shallow embedding of temporal operators over Boolean streams. This connects the specialised world of trajectory evaluation to a general-purpose (HOL-like) logic and gives a semantic basis for interfacing model-checking and theorem-proving.

This is joint work with Mark Aagaard and John O'Leary at the Strategic CAD Labs, Intel.

Lunch

For those interested in lunch, please contact Carron, ces@cs.stir.ac.uk. Food on campus is not great, but there's a nice pub nearby, and for those with cars, a very nice restaurant near the motor way (this is much better than it sounds - honest).

Travel

There is a map of the campus and surrounding area at

http://www.cs.stir.ac.uk/~kjt/general/univ.html

If coming by car, the main car park is at the back of the Cottrell Building.

If you're coming by train, get the train to Stirling station and either take a taxi (it should only cost 4 - 5 pounds) or the bus to the University (costs 1 pound, there are several, and most of them say University on them). Come out of the train station, cross the road and go up the road to your left. At the top turn right. The bus stops are about 50 yards ahead (left hand side of the road). The second one is the University one. The journey takes about 10 minutes.The bus stops right outside the Cottrell Building.

Alternatively, get the train to Bridge of Allan and walk back along the main road to the University (25 minutes).

Inside Cottrell: Enter by the main entrance in Queens Court. Go through the double doors ahead of you and turn left. Through another set of double doors and A1 is the lecture theatre on the left.

Return to Scottish Theorem Proving page.