The arrival of Melham in 2002, followed by Ouaknine in 2004, greatly raised the profile of verification research in the Laboratory. The subsequent appointments of Kroening, Kwiatkowska, and Worrell have consolidated this into a world-class verification group at Oxford. We emphasize practical, machine-assisted methods applicable to real-world problems and languages, and have strong industrial links. Our major strengths include abstraction, industrial-scale hardware verification, software model-checking, verification of real-time and probabilistic systems - with Norman leading on systems that are both probabilistic and real-time. Probabilistic verification has successful applications in security protocols, power management, nanotechnology, and biology. Notable achievements include Ouaknine's extension of the ANSI-C model checker MAGIC to concurrent systems, together with new algorithms to look for deadlocks in concurrent C programs. This was used to discover bugs in the Micro-C/OS II operating system, found in avionics systems, medical equipment, nuclear installations, and hundreds of other products. Ouaknine and his colleagues also found errors in a multi-threaded robotics control automation system that had gone undetected despite seven years of industrial use. Melham worked in close collaboration with Intel on their Forte verification system, which became well-established within the company for floating-point and other datapath verifications. Kroening was granted a US patent (7,225,417) for a new method to establish consistency between C and HDL descriptions of hardware.
