Posted: 21st December 2011

Oxford’s Daniel Kroening has been recognised with  the 2011 Haifa Verification Conference award for work on CBMC, a bounded model-checker for C programs. The HVC award recognizes the most promising academic and industrial contribution to the fields of testing and software and hardware verification from the last five years.

CMBC is the first and most influential industrial-strength verification engine for a non-academic programming language, and hence a major milestone in automated verification. To date, CMBC is the only verification engine that supports the full functionality of C, including precise modeling of floating-point operations and bit-precise arithmetic.

In recognising Daniel's achievements, the awarding body stated:

“Previous verification engines for programs, better known as theorem provers, were all dedicated to artificial languages and required manual assistance in the form of invariants and intermediate goals. Their focus was not necessarily on programs or industrial adoption. Indeed, these tools are rarely used in the industry.

In contrast, CBMC is being used in dozens of locations in the industry around the world. Several bugs in MS-Windows, for example, were exposed in Microsoft with modules of CBMC. CBMC is based on continuous innovation, developed and implemented by Daniel  and his group. Other tools developed by Daniel include SATABS and EBMC, which are used in the industry as well, and together they provide an extremely comprehensive software verification solution.

Research is taking place around CBMC in almost every research university in the US and Europe. The main CBMC article is cited (according to Google Scholar) over 400 times to date. It is safe to say that CBMC promotes the industrial adoption of formal software verification more than any other tool in existence.”

Daniel presented his award-winning contribution at the IBM-organised conference in Haifa, Israel earlier this month.  HVC 2011 was the seventh in the series of annual conferences dedicated to advancing the state-of the-art and state-of-the-practice in verification and testing of hardware and software. The conference provides a forum for researchers and practitioners from both academia and industry to share their work, exchange ideas, and discuss challenges and future directions of testing and verification for hardware, software, and hybrid systems.