Design patterns have been used by object oriented architects and developers to design and build systems for many years. However, as systems evolve, code is changed and design patterns may be broken inadvertently.

I will present my work with Hedgehog, a system that is designed to verify design patterns in Java code, and the use that this may have in long term projects.

We outline the design and implementation of an interface between the Maple6 computer algebra system and the PVS  automated proof sytem. We also demonstrate its use in the verification of computer algebra results.

Despite Java's many good points, its interpreted nature means that it is not particularly fast or efficient; the use of Just In Time  (JIT) Compilers is one way to combat this problem. The aim of my work is to enable JIT compilers to make optimizations not currently possible, and to perform existing optimizations more efficiently, by proving that certain properties hold of Java bytecode programs. With this in mind, I will discuss the development of a Programming Logic for bytecode programs, building on work done by Cornelia Pusch on the formalisation of the operational semantics of Java using the Isabelle theorem prover.

Model checking is a popular validation technique because it is seen as easy to use. The main problem is that only specific scenarios of finite size can be checked, therefore lots of people are tackling the problem of how to generalise the results from model checking to infinite state, or how to make the model checkers deal with infinite state in some way. We have developed a theory in which transition systems can be represented in a finite way (presented at the December STP), namely Symbolic Transition Systems (STSs). We've also defined a logic over STSs. In this talk I'll present work on implementing prototype model checkers using a variety of different techniques: XTL and the CADP toolkit, the theorem prover Ergo which allows interactive proofs in a generalised sequent calculus style, and Rewriting Logic using Maude.