December 6-8, 2011
Tutorials: December 5, 2011
Organized by IBM R&D Labs in Israel

Granted since 2007, 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.

The HVC award committee considered ten strong candidates with both academic and industrial impact. In the end, the committee decided to grant the 2011 award to Prof. Daniel Kroening from Oxford for his contribution of CBMC, a bounded model-checker for C programs. 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.

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 Prof. Kroening and his group. Other tools developed by Prof. Kroening, such as SATABS and EBMC, 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.

Prof. Kroening will present his award-winning contribution at the conference.

HVC Award committee:

• Shmuel Ur, Ur-Innovation (Chair)
• Ian G. Harris, University of California Irvine
• Klaus Havelund, JPL
• Mika Katara, Tampere University of Technology
• Ofer Strichman, Technion