Computer Laboratory

Old ACS project suggestions

Project suggestions from the Programming, Logic and Semantics Group

Analyzing Real-World Testing Practice

Supervisor: Alastair Beresford

Originator & Day-to-day supervisor: Kathy Gray

Software testing is an important part of software development; however, developing tests can be an expensive and error prone process. Improved tools can simplify test development but should be based on real world practice. Identifying how programmers specify correctness properties in tests requires analyzing a program and its test suite.

This project is to develop a tool to analyze Java programs and extract information on test specifications. This will include method-level coverage, percentages of different styles of tests that occur, and extracting example tests that suggest atypical practices.

Tests in Java range from simple uses of the JUnit API such as

@test distance {
   Map m = Map.setup();
   assertEquals(m.distance("Cambridge", "London"), 60);

to complex programs with nested try blocks, cloned and copied values, and manual assertions of success and failure. The analysis should distinguish between tested methods, such as distance, and methods used as predicates to aid the test.

The tool will traverse a Java AST, generated using the front-end of an open-source Java compiler such as jastAddJ or Polyglot. Analysis will examine real world open-source Java applications such as Eclipse, Java-portions of, ant, and others.

This work contributes to on-going research in the CPRG on test specifications (based on a limited manual analysis of real programs) and test development.

An SMT-based tool for exploration of relaxed memory models

Supervisor: Peter Sewell

Originator & Day-to-day supervisor: Susmit Sarkar / Jaroslav Sevcik / Peter Sewell

Multiprocessors (such as x86, Power6, ARM, Sparc, and Itanium) and high-level languages (such as Java and C++0x) typically provide only relaxed or weakly consistent views of the shared memory to different threads. Exactly what is guaranteed is a subtle question that differs wildly between architectures and languages, and for many is not yet well-understood. Some preliminary research in this area is here, and we have ongoing discussions with some processor designers and low-level concurrent software people.

This project is to develop a tool to explore the consequences of an axiomatically specified memory model: to take a set of memory model axioms and an example test program and calculate the set of all allowed executions. It should probably accept axioms written in a subset of the HOL4 proof assistant language, make use of an SMT solver for the back-end, and have a good user interface to make it a usable research tool. We have an existing prototype tool that should provide inspiration, and possibly code, to build upon.

One could go on to work on a new formal memory model, perhaps for Itanium, analyse its consequences using the tool, and develop theoretical results (for example, showing that race-free programs behave well).

The project would suit someone with an interest in both semantics and computer systems.