Cottrell Building,

University of Stirling

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 |

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.

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.

(Joint work with Gottliebsen, Linton and Martin.)

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

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. |