|1400 - 1440|| "A Quick SPIN around Model-Checking"|
University of Glasgow
|1440 - 1500|| "Test Case Extraction from Correctness Proofs"|
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"|
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.
This is joint work with Mark Aagaard and John O'Leary at the Strategic CAD Labs, Intel.
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.|