Department of Computing Seminars 1999/2000
Problem Structure and Analysis
Tuesday 5 October - Michael Jackson:
Introduction to Secret Codes and Digital Signatures
Tuesday 19th October and Wednesday 20th October 1999 - Nigel Smart, Hewlett Packard:
I will explain, to a general audience, the basics of the modern science
of cryptography. I will discuss various real world scenarios where
codes and signatures are needed to ensure electronic commerce. I will
explain the background behind some of the public policy decisions
facing governments today. Finally I will look to the future to see
where we are going and what problems need to be tackled. I will assume
no background from the audience, hence the talk will be applicable to
anybody from A-Level student upwards.
An Implementation of Amorphous Program Slicing
5pm, Thursday 21st October 1999 - David Binkley [Loyola College]:
Traditional program slicing simplifies a program by deleting statements
and expressions which do not affect a computation of interest in the
program. The simplification power of traditional slicing is limited by
the restriction to deletion as the only simplifying transformation.
Amorphous program slicing retains the semantic property that a slice
preserves a projection of the original program's behavior, but drops
the syntactic requirement that the slice is a syntactic subset of the
original program. This allows for greater simplification, improving the
applicability of slicing to problems where syntax is relatively
unimportant.
An implementation of amorphous slicing based on a program's system
dependence graph is described. The system dependence graph is an idea
representation for computing amorphous slices as it contains sufficient
information to compute traditional slices and to perform other
transformations that are part of amorphous slicing. CodeSurfer, a
software analysis tool, is used to produce a program's system
dependence graph. This graph is then fed to a C program that performs
traditional slicing and semantics preserving graph transformations.
The current implementation addresses the problem of array access
safety. Preliminary results obtained from the implementation using
several small programs are presented along with the data from a
prototype experiment designed to look into amorphous slicing's ability
to assist a maintenance engineer in isolating certain kinds of faults.
Reducing the Cost of Regression Testing
5pm, Friday 22nd October 1999 - David Binkley [Loyola College]:
Software maintainers are faced with the task of regression testing:
retesting a modified program on an often large number of test cases.
The cost of regression testing can be reduced if the size of the
program that must be retested is reduced and if old test cases and old
test results can be reused. Two complimentary algorithms for reducing
the cost of regression testing are presented. The first produces a
program named `differences', which captures the semantic change between
`certified', a previously tested program, and `modified', a changed
version of `certified'.
It is more efficient to test differences, because this omits unchanged
computations of modified. This algorithm is based on the semantic
properties of program slices. Essentially, two programs that share a
slice share a computation.
The second algorithm identifies test cases for which `certified' and
`modified' will produce the same output and existing test cases that
will test components which are new to `modified'. Not rerunning test
cases that produce the same output avoids unproductive testing. This
algorithm is based on the notion of common execution patterns. Program
components with common execution patterns have the same execution
pattern during some call to their respective procedures.
Together with `differences', it becomes possible to test `modified' by
running the smaller program `differences' on a smaller number of test
cases. This should be more efficient than running `modified' on a
larger number of test cases.
A prototype implementation of the first algorithm, which takes C
programs as its input, has recently been completed. The prototype
combines two code analysis tools: Cdiff and CodeSurfer. Cdiff is used
to identify the meaningful syntactic differences between two C
programs. CodeSurfer is a code analysis tool that produces and slices
system dependence graphs. Though a scheme API, it is possible to extend
CodeSurfer. The core of the computation of differences is carried out
by a collection of scheme functions.
The implementation is being used in experiments to measure the
effectiveness of the `differences' program. The first experiment deals
with the size of `differences' when compared to the size of `modified'.
Experiments are planned on a collection of C programs ranging from just
under 200 lines of code to around 50,000 lines of code.
An implementation of the second algorithm for a small toy languages
also exists. Preliminary data obtained from experiments with the two
implementations will be presented.
Some extremal problems in approximation theory
Tuesday 9th November 1999 - Christina Dragonova Sofia University/UCL:
Animating the Semantics of VERILOG using Prolog
Tuesday 16th November 1999 - Jonathan Bowen, University of Reading:
The logic programming language Prolog is used to provide a
rapid-prototype simulator for the VERILOG Hardware Description Language
(HDL). The simulator is based on an operational semantics of a
significant subset of the language. Using this approach allows the
exploration of sometimes subtle behaviours of parallel programs and the
possibility of rapid changes or additions to the semantics of the
language covered. It also acts as a check on the validity of the
original operational semantics.
Codes, trellises and matroids
Tuesday 30 November 1999 - Peter Cammeron, Queen Mary and Westfield:
There is a very close link between linear codes and representable
matroids: given a matrix, the rows span the code, and the columns
represent the matroid. Information can be transferred back and forth
between code and matroid. For example, Greene showed that the weight
enumerator of the code is a specialisation of the Tutte polynomial of
the matroid. Trellises provide a method for decoding a linear code used
over an analog transmission line without the need for analog-to-digital
conversion. It is important to be able to find the smallest trellis
which represents a given code. This invariant, unlike more familiar
ones, depends on the order of the coordinates; it is not invariant
under permutations of coordinates. Nevertheless, it can be calculated
from the matroid in a natural way. The talk will be an elementary
exposition of these ideas, with several illustrative examples.
Testing the safety of a computer-controlled railway signalling device
Tuesday 14th December 1999 - Jim Woodcock, Oxford University (PRG):
Domain Theory and Analytic Sets
Tuesday 8th February 2000 - John Howroyd, Goldsmiths College:
Efficient Strategies for Selective Mutation Testing
Tuesday 14th March 2000 - Len Bottaci, Hull University:
The talk introduces the mutation testing technique for unit testing of
software and the notion of test set efficiency. The various forms of
selective mutation testing are described in terms of their
effectiveness and cost saving. A heuristic for efficient operator
selective mutation is proposed. With the aim of finding efficient
selective mutation testing strategies, operator selective mutation is
compared to random selective mutation in an experiment using 11
programs. It turns out that the choice of most efficient strategy
depends on the degree of testing confidence required.
Indexing texts and data compression
Wednesday 15th March 2000 - Professor Maxime Crochemore , University of Marne-la-Vallée:
Tuesday 21th March 2000 - Simon Burton, York University:
This presentation describes the intermediate results of a project to develop automated, high integrity, software verification and validation techniques for aerospace applications. Automated specification validation and test case generation are made possible by the targeted use of formal methods. Specifically, the restricted domain of use is exploited to reduce the set of mathematical problems to those that can be solved using constraint solvers, model checkers and automated proof tactics. The practicality of the technique is enhanced by the tight integration of the formal methods to intuitive specification notations, existing specification modelling tools and a traditional software development process. This paper presents evidence to support an emerging appreciation amongst the software engineering community that, for the benefits of formal methods to be widely exploited in industry, an approach must be taken that integrates formal analysis with intuitive engineering notations, traditional engineering approaches and powerful tool support.