Hardware Verification

The arrival of Melham in 2002, followed by Ouaknine in 2004, greatly raised the profile of verification research in the Laboratory (now the Department of Computer Science). 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.

Selected Publications

View All

• Automated Pipeline Design

  Daniel Kroening and Wolfgang Paul

  In Proc. of 38th ACM/IEEE Design Automation Conference (DAC 2001). Pages 810–815. ACM Press. 2001.

  Details about Automated Pipeline Design | BibTeX data for Automated Pipeline Design

• Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog

  Himanshu Jain‚ Daniel Kroening‚ Natasha Sharygina and Edmund Clarke

  In IEEE Transactions on Computer−Aided Design of Integrated Circuits and Systems (TCAD). Vol. 27. Pages 366–379. February, 2008.

  Details about Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog | BibTeX data for Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog